1 /-
2 Copyright (c) 2018 Mario Carneiro. All rights reserved.
3 Released under Apache 2.0 license as described in the file LICENSE.
4 Authors: Mario Carneiro, Sean Leather
5
6 Functions on lists of sigma types.
7 -/
8 import data.list.perm data.sigma
src └────────────┘ └────────┘
9
10 universes u v
11
12 namespace list
13 variables {α : Type u} {β : α → Type v}
14
15 /- keys -/
16
17 /-- List of keys from a list of key-value pairs -/
18 def keys : list (sigma β) → list α :=
id └──┘ └───┘ ┴ └──┘ ┴
src └──┘ └───┘ └──┘
typ └──┘ └───┘ ┴ └──┘ ┴
19 map sigma.fst
id └─┘ └───────┘
src └─┘ └───────┘
typ └─┘ └───────┘
20
21 @[simp] theorem keys_nil : @keys α β [] = [] :=
id └──┘ ┴ ┴ └┘ ┴ └┘
src └──┘ └┘ ┴ └┘
typ └──┘ ┴ ┴ └┘ ┴ └┘
doc └──┘ └──┘
22 rfl
id └─┘
src └─┘
typ └─┘
23
24 @[simp] theorem keys_cons {s} {l : list (sigma β)} : (s :: l).keys = s.1 :: l.keys :=
id └──┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴┴ └┘ ┴└───┘
src └──┘ └───┘ └┘ └──┘ ┴ ┴ └┘ └───┘
typ └──┘ └───┘ ┴ ┴ └┘ ┴ └──┘ ┴ ┴┴ └┘ ┴└───┘
doc └──┘ └──┘ └───┘
25 rfl
id └─┘
src └─┘
typ └─┘
26
27 theorem mem_keys_of_mem {s : sigma β} {l : list (sigma β)} : s ∈ l → s.1 ∈ l.keys :=
id └───┘ ┴ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴└───┘
src └───┘ └──┘ └───┘ ┴ ┴ ┴ └───┘
typ └───┘ ┴ └──┘ └───┘ ┴ ┴ ┴ ┴ ┴┴ ┴ ┴└───┘
doc └───┘
28 mem_map_of_mem sigma.fst
id └────────────┘ └───────┘
src └────────────┘ └───────┘
typ └────────────┘ └───────┘
29
30 theorem exists_of_mem_keys {a} {l : list (sigma β)} (h : a ∈ l.keys) :
id └──┘ └───┘ ┴ ┴ ┴ ┴└───┘
src └──┘ └───┘ ┴ └───┘
typ └──┘ └───┘ ┴ ┴ ┴ ┴└───┘
doc └───┘
31 ∃ (b : β a), sigma.mk a b ∈ l :=
id ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ ┴ └──────┘ ┴
typ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
32 let ⟨⟨a', b'⟩, m, e⟩ := exists_of_mem_map h in
id └─┘ └┘ ┴ ┴ └───────────────┘ ┴
src └───────────────┘
typ └─┘ └┘ ┴ ┴ └───────────────┘ ┴
33 eq.rec_on e (exists.intro b' m)
id └───────┘ └──────────┘
src └───────┘ └──────────┘
typ └───────┘ └──────────┘
34
35 theorem mem_keys {a} {l : list (sigma β)} : a ∈ l.keys ↔ ∃ (b : β a), sigma.mk a b ∈ l :=
id └──┘ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └───┘ ┴ └───┘ ┴ ┴ ┴ └──────┘ ┴
typ └──┘ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └───┘
36 ⟨exists_of_mem_keys, λ ⟨b, h⟩, mem_keys_of_mem h⟩
id └────────────────┘ ┴ ┴ └─────────────┘
src └────────────────┘ └─────────────┘
typ └────────────────┘ ┴ ┴ └─────────────┘
37
38 theorem not_mem_keys {a} {l : list (sigma β)} : a ∉ l.keys ↔ ∀ b : β a, sigma.mk a b ∉ l :=
id └──┘ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └───┘ ┴ └───┘ ┴ └──────┘ ┴
typ └──┘ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └───┘
39 (not_iff_not_of_iff mem_keys).trans not_exists
id └────────────────┘ └──────┘ └───┘ └────────┘
src └────────────────┘ └──────┘ └───┘ └────────┘
typ └────────────────┘ └──────┘ └───┘ └────────┘
40
41 theorem not_eq_key {a} {l : list (sigma β)} : a ∉ l.keys ↔ ∀ s : sigma β, s ∈ l → a ≠ s.1 :=
id └──┘ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
src └──┘ └───┘ ┴ └───┘ ┴ └───┘ ┴ ┴ ┴
typ └──┘ └───┘ ┴ ┴ ┴ ┴└───┘ ┴ └───┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴┴
doc └───┘
42 iff.intro
id └───────┘
src └───────┘
typ └───────┘
43 (λ h₁ s h₂ e, absurd (mem_keys_of_mem h₂) (by rwa e at h₁))
id └┘ ┴ └┘ ┴ └────┘ └─────────────┘ └┘ ┴
src └────┘ └─────────────┘ └──┘ └────┘
typ └┘ ┴ └┘ ┴ └────┘ └─────────────┘ └┘ └──┘┴└────┘
doc └──┘ └────┘
txt └──┘ └────┘
par └──┘ └────┘
pid ┴ └────┘
st └──────────┘
44 (λ f h₁, let ⟨b, h₂⟩ := exists_of_mem_keys h₁ in f _ h₂ rfl)
id ┴ └┘ └─┘ └┘ └────────────────┘ └┘ ┴ └─┘
src └────────────────┘ └─┘
typ ┴ └┘ └─┘ └┘ └────────────────┘ └┘ ┴ └─┘
45
46 /- nodupkeys -/
47
48 def nodupkeys (l : list (sigma β)) : Prop :=
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
49 l.keys.nodup
id ┴└───┘└────┘
src └───┘└────┘
typ ┴└───┘└────┘
doc └───┘└────┘
50
51 theorem nodupkeys_iff_pairwise {l} : nodupkeys l ↔
id └───────┘ ┴ ┴
src └───────┘ ┴
typ └───────┘ ┴ ┴
52 pairwise (λ s s' : sigma β, s.1 ≠ s'.1) l := pairwise_map _
id └──────┘ └───┘ ┴ ┴┴ ┴ └┘┴ ┴ └──────────┘
src └──────┘ └───┘ ┴ ┴ ┴ └──────────┘
typ └──────┘ └───┘ ┴ ┴┴ ┴ └┘┴ ┴ └──────────┘
doc └──────┘
53
54 @[simp] theorem nodupkeys_nil : @nodupkeys α β [] := pairwise.nil
id └───────┘ ┴ ┴ └┘ └──────────┘
src └───────┘ └┘ └──────────┘
typ └───────┘ ┴ ┴ └┘ └──────────┘
doc └──┘
55
56 @[simp] theorem nodupkeys_cons {s : sigma β} {l : list (sigma β)} :
id └───┘ ┴ └──┘ └───┘ ┴
src └───┘ └──┘ └───┘
typ └───┘ ┴ └──┘ └───┘ ┴
doc └──┘
57 nodupkeys (s::l) ↔ s.1 ∉ l.keys ∧ nodupkeys l :=
id └───────┘ ┴└┘┴ ┴ ┴┴ ┴ ┴└───┘ ┴ └───────┘ ┴
src └───────┘ └┘ ┴ ┴ ┴ └───┘ ┴ └───────┘
typ └───────┘ ┴└┘┴ ┴ ┴┴ ┴ ┴└───┘ ┴ └───────┘ ┴
doc └───┘
58 by simp [keys, nodupkeys]
id └──┘ └───────┘
src └────┘└──┘└┘└───────┘└─
typ └────┘└──┘└┘└───────┘└─
doc └────┘└──┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └───────────────────────
59
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
60 theorem nodupkeys.eq_of_fst_eq {l : list (sigma β)}
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
61 (nd : nodupkeys l) {s s' : sigma β} (h : s ∈ l) (h' : s' ∈ l) :
id └───────┘ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
src └───────┘ └───┘ ┴ ┴
typ └───────┘ ┴ └───┘ ┴ ┴ ┴ ┴ └┘ ┴ ┴
62 s.1 = s'.1 → s = s' :=
id ┴┴ ┴ └┘┴ ┴ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴┴ ┴ └┘┴ ┴ ┴ └┘
63 @forall_of_forall_of_pairwise _
id └──────────────────────────┘
src └──────────────────────────┘
typ └──────────────────────────┘
64 (λ s s' : sigma β, s.1 = s'.1 → s = s')
id └───┘ ┴ ┴┴ ┴ └┘┴ ┴ ┴ └┘
src └───┘ ┴ ┴ ┴ ┴
typ └───┘ ┴ ┴┴ ┴ └┘┴ ┴ ┴ └┘
65 (λ s s' H h, (H h.symm).symm) _ (λ x h _, rfl)
id ┴ └┘ ┴ ┴ ┴ ┴└───┘ └──┘ ┴ ┴ ┴ └─┘
src └───┘ └──┘ └─┘
typ ┴ └┘ ┴ ┴ ┴ ┴└───┘ └──┘ ┴ ┴ ┴ └─┘
66 ((nodupkeys_iff_pairwise.1 nd).imp (λ s s' h h', (h h').elim)) _ h _ h'
id └────────────────────┘┴ └┘ └─┘ ┴ └┘ ┴ └┘ ┴ └┘ └──┘ ┴ └┘
src └────────────────────┘┴ └─┘ └──┘
typ └────────────────────┘┴ └┘ └─┘ ┴ └┘ ┴ └┘ ┴ └┘ └──┘ ┴ └┘
67
68 theorem nodupkeys.eq_of_mk_mem {a : α} {b b' : β a} {l : list (sigma β)}
id ┴ ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴
69 (nd : nodupkeys l) (h : sigma.mk a b ∈ l) (h' : sigma.mk a b' ∈ l) : b = b' :=
id └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
src └───────┘ └──────┘ ┴ └──────┘ ┴ ┴
typ └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ └┘ ┴ ┴ ┴ ┴ └┘
70 by cases nd.eq_of_fst_eq h h' rfl; refl
id └─────────────┘ ┴ └┘ └─┘
src └────┘└─────────────┘┴ ┴ ┴└─┘ └────
typ └────┘└─────────────┘┴┴┴└┘┴└─┘ └────
doc └────┘ ┴ ┴ ┴ └────
txt └────┘ ┴ ┴ ┴ └────
par └────┘ ┴ ┴ ┴ └────
pid ┴ ┴ ┴ ┴ └
st └─────────────────────────────────────
71
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
72 theorem nodupkeys_singleton (s : sigma β) : nodupkeys [s] := nodup_singleton _
id └───┘ ┴ └───────┘ ┴┴┴ └─────────────┘
src └───┘ └───────┘ ┴ ┴ └─────────────┘
typ └───┘ ┴ └───────┘ ┴┴┴ └─────────────┘
73
74 theorem nodupkeys_of_sublist {l₁ l₂ : list (sigma β)} (h : l₁ <+ l₂) : nodupkeys l₂ → nodupkeys l₁ :=
id └──┘ └───┘ ┴ └┘ └┘ └┘ └───────┘ └┘ └───────┘ └┘
src └──┘ └───┘ └┘ └───────┘ └───────┘
typ └──┘ └───┘ ┴ └┘ └┘ └┘ └───────┘ └┘ └───────┘ └┘
75 nodup_of_sublist (map_sublist_map _ h)
id └──────────────┘ └─────────────┘ ┴
src └──────────────┘ └─────────────┘
typ └──────────────┘ └─────────────┘ ┴
76
77 theorem nodup_of_nodupkeys {l : list (sigma β)} : nodupkeys l → nodup l :=
id └──┘ └───┘ ┴ └───────┘ ┴ └───┘ ┴
src └──┘ └───┘ └───────┘ └───┘
typ └──┘ └───┘ ┴ └───────┘ ┴ └───┘ ┴
doc └───┘
78 nodup_of_nodup_map _
id └────────────────┘
src └────────────────┘
typ └────────────────┘
79
80 theorem perm_nodupkeys {l₁ l₂ : list (sigma β)} (h : l₁ ~ l₂) : nodupkeys l₁ ↔ nodupkeys l₂ :=
id └──┘ └───┘ ┴ └┘ ┴ └┘ └───────┘ └┘ ┴ └───────┘ └┘
src └──┘ └───┘ ┴ └───────┘ ┴ └───────┘
typ └──┘ └───┘ ┴ └┘ ┴ └┘ └───────┘ └┘ ┴ └───────┘ └┘
doc ┴
81 perm_nodup $ perm_map _ h
id └────────┘ └──────┘ ┴
src └────────┘ └──────┘
typ └────────┘ └──────┘ ┴
82
83 theorem nodupkeys_join {L : list (list (sigma β))} :
id └──┘ └──┘ └───┘ ┴
src └──┘ └──┘ └───┘
typ └──┘ └──┘ └───┘ ┴
84 nodupkeys (join L) ↔ (∀ l ∈ L, nodupkeys l) ∧ pairwise disjoint (L.map keys) :=
id └───────┘ └──┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └──────┘ └──────┘ ┴└──┘ └──┘
src └───────┘ └──┘ ┴ ┴ └───────┘ ┴ └──────┘ └──────┘ └──┘ └──┘
typ └───────┘ └──┘ ┴ ┴ ┴ ┴ └───────┘ ┴ ┴ └──────┘ └──────┘ ┴└──┘ └──┘
doc └──────┘ └──────┘ └──┘
85 begin
st └─────
86 rw [nodupkeys_iff_pairwise, pairwise_join, pairwise_map],
id └────────────────────┘ └───────────┘ └──────────┘
src └──┘└────────────────────┘└┘└───────────┘└┘└──────────┘┴
typ └──┘└────────────────────┘└┘└───────────┘└┘└──────────┘┴
doc └──┘ └┘ └┘ ┴
txt └──┘ └┘ └┘ ┴
par └──┘ └┘ └┘ ┴
pid └┘ └┘ └┘ ┴
st ───────────────────────────┘└─────────────┘└────────────┘└──
87 refine and_congr (ball_congr $ λ l h, by simp [nodupkeys_iff_pairwise]) _,
id └───────┘ └────────┘ └────────────────────┘
src └─────┘└───────┘┴ └────────┘┴ ┴ └────┘ ┴└────┘└────────────────────┘┴└─┘
typ └─────┘└───────┘┴ └────────┘┴ ┴ └────┘ ┴└────┘└────────────────────┘┴└─┘
doc └─────┘ ┴ ┴ ┴ └────┘ ┴└────┘ ┴└─┘
txt └─────┘ ┴ ┴ ┴ └────┘ ┴└────┘ ┴└─┘
par └─────┘ ┴ ┴ ┴ └────┘ ┴└────┘ ┴└─┘
pid ┴ ┴ ┴ ┴ └────┘ └─────┘ └──┘
st ─────────────────────────────────────────┘└────────────────────────────┘└─┘└─
88 apply iff_of_eq, congr', ext l₁ l₂,
id └───────┘
src └────┘└───────┘ └────┘ └───────┘
typ └────┘└───────┘ └────┘ └───────┘
doc └────┘ └────┘ └───────┘
txt └────┘ └────┘ └───────┘
par └────┘ └────┘ └───────┘
pid ┴ └────┘
st ────────────────┘└──────┘└─────────┘└─
89 simp [keys, disjoint_iff_ne]
id └──┘ └─────────────┘
src └────┘└──┘└┘└─────────────┘└┘
typ └────┘└──┘└┘└─────────────┘└┘
doc └────┘└──┘└┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ──────────────────────────────┘
90 end
st └─┘
91
92 theorem nodup_enum_map_fst (l : list α) : (l.enum.map prod.fst).nodup :=
id └──┘ ┴ ┴└───┘└──┘ └──────┘ └───┘
src └──┘ └───┘└──┘ └──────┘ └───┘
typ └──┘ ┴ ┴└───┘└──┘ └──────┘ └───┘
doc └───┘
93 by simp [list.nodup_range]
id └──────────────┘
src └────┘└──────────────┘└─
typ └────┘└──────────────┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └────────────────────────
94
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
95 variables [decidable_eq α]
id └──────────┘
src └──────────┘
typ └──────────┘
96
97 /- lookup -/
98
99 /-- `lookup a l` is the first value in `l` corresponding to the key `a`,
100 or `none` if no such element exists. -/
101 def lookup (a : α) : list (sigma β) → option (β a)
id ┴ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴
src └──┘ └───┘ └────┘
typ ┴ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴
102 | [] := none
id └┘ └──┘
src └┘ └──┘
typ └┘ └──┘
103 | (⟨a', b⟩ :: l) := if h : a' = a then some (eq.rec_on h b) else lookup l
id └┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘ └───────┘ ┴ └────┘
src └┘ └┘ ┴ └──┘ └───────┘ └────┘
typ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └──┘ └───────┘ ┴ └────┘
104
105 @[simp] theorem lookup_nil (a : α) : lookup a [] = @none (β a) := rfl
id ┴ └────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └─┘
src └────┘ └┘ ┴ └──┘ └─┘
typ ┴ └────┘ ┴ └┘ ┴ └──┘ ┴ ┴ └─┘
doc └──┘ └────┘
st ┴
106
107 @[simp] theorem lookup_cons_eq (l) (a : α) (b : β a) : lookup a (⟨a, b⟩::l) = some b :=
id ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘┴ ┴ └──┘ ┴
src └────┘ └┘ ┴ └──┘
typ ┴ ┴ ┴ └────┘ ┴ ┴ ┴ └┘┴ ┴ └──┘ ┴
doc └──┘ └────┘
108 dif_pos rfl
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
109
110 @[simp] theorem lookup_cons_ne (l) {a} :
doc └──┘
111 ∀ s : sigma β, a ≠ s.1 → lookup a (s::l) = lookup a l
id ┴ └───┘ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴└┘┴ ┴ └────┘ ┴ ┴
src └───┘ ┴ ┴ └────┘ └┘ ┴ └────┘
typ ┴ └───┘ ┴ ┴ ┴ ┴┴ └────┘ ┴ ┴└┘┴ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
112 | ⟨a', b⟩ h := dif_neg h.symm
id ┴ └─────┘ └───┘
src └─────┘ └───┘
typ ┴ └─────┘ └───┘
113
114 theorem lookup_is_some {a : α} : ∀ {l : list (sigma β)},
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
115 (lookup a l).is_some ↔ a ∈ l.keys
id └────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴└───┘
src └────┘ └─────┘ ┴ ┴ └───┘
typ └────┘ ┴ ┴ └─────┘ ┴ ┴ ┴ ┴└───┘
doc └────┘ └───┘
116 | [] := by simp
id └┘
src └┘ └───┘
typ └┘ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
117 | (⟨a', b⟩ :: l) := begin
id └┘
src └┘
typ └┘
st └─────
118 by_cases h : a = a',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
119 { subst a', simp },
id └┘
src └────┘ └───┘
typ └────┘└┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ───┘└──────┘└─────┘└┘└
120 { simp [h, lookup_is_some] },
id ┴
src └────┘ └┘ └┘
typ └────┘┴└┘└────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ────────────────────────────┘└──
121 end
st ──┘
122
123 theorem lookup_eq_none {a : α} {l : list (sigma β)} :
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
124 lookup a l = none ↔ a ∉ l.keys :=
id └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴└───┘
src └────┘ ┴ └──┘ ┴ ┴ └───┘
typ └────┘ ┴ ┴ ┴ └──┘ ┴ ┴ ┴ ┴└───┘
doc └────┘ └───┘
125 begin
st └─────
126 have := not_congr (@lookup_is_some _ _ _ a l),
id └───────┘ └────────────┘ ┴ ┴
src └──────┘└───────┘┴ └────────────┘└─────┘ ┴ ┴
typ └──────┘└───────┘┴ └────────────┘└─────┘┴┴┴┴
doc └──────┘ ┴ └─────┘ ┴ ┴
txt └──────┘ ┴ └─────┘ ┴ ┴
par └──────┘ ┴ └─────┘ ┴ ┴
pid └───┘└─┘ ┴ └─────┘ ┴ ┴
st ──────────────────────────────────────────────┘└─
127 simp at this, refine iff.trans _ this,
id └───────┘ └──┘
src └──────────┘ └─────┘└───────┘└─┘
typ └──────────┘ └─────┘└───────┘└─┘└──┘
doc └──────────┘ └─────┘ └─┘
txt └──────────┘ └─────┘ └─┘
par └──────────┘ └─────┘ └─┘
pid ┴└─────┘ ┴ └─┘
st ─────────────┘└───────────────────────┘└─
128 cases lookup a l; exact dec_trivial
id └────┘ ┴ ┴ └─────────┘
src └────┘└────┘┴ ┴ └────┘└─────────┘┴
typ └────┘└────┘┴┴┴┴ └────┘└─────────┘┴
doc └────┘└────┘┴ ┴ └────┘└─────────┘┴
txt └────┘ ┴ ┴ └────┘ ┴
par └────┘ ┴ ┴ └────┘ ┴
pid ┴ ┴ ┴ ┴ ┴
st ─────────────────────────────────────┘
129 end
st └─┘
130
131 theorem of_mem_lookup
132 {a : α} {b : β a} : ∀ {l : list (sigma β)}, b ∈ lookup a l → sigma.mk a b ∈ l
id ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └───┘ ┴ └────┘ └──────┘ ┴
typ ┴ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴ ┴ └────┘ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └────┘
133 | (⟨a', b'⟩ :: l) H := begin
id └┘
src └┘
typ └┘
st └─────
134 by_cases h : a = a',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
135 { subst a', simp at H, simp [H] },
id └┘ ┴
src └────┘ └───────┘ └────┘ └┘
typ └────┘└┘ └───────┘ └────┘┴└┘
doc └────┘ └───────┘ └────┘ └┘
txt └────┘ └───────┘ └────┘ └┘
par └────┘ └───────┘ └────┘ └┘
pid ┴ ┴└──┘ ┴┴ ┴┴
st ───┘└──────┘└─────────┘└─────────┘└┘└
136 { simp [h] at H, exact or.inr (of_mem_lookup H) }
id ┴ └────┘ └───────────┘ ┴
src └────┘ └────┘ └────┘└────┘┴ ┴ └┘
typ └────┘┴└────┘ └────┘└────┘┴ └───────────┘┴┴└┘
doc └────┘ └────┘ └────┘ ┴ ┴ └┘
txt └────┘ └────┘ └────┘ ┴ ┴ └┘
par └────┘ └────┘ └────┘ ┴ ┴ └┘
pid ┴┴ ┴┴└──┘ ┴ ┴ ┴ ┴┴
st ────────────────┘└───────────────────────────────┘└─
137 end
st ──┘
138
139 theorem mem_lookup {a} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys)
id ┴ ┴ └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ ┴ ┴ └──┘ └───┘ ┴ ┴└────────┘
140 (h : sigma.mk a b ∈ l) : b ∈ lookup a l :=
id └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
src └──────┘ ┴ ┴ └────┘
typ └──────┘ ┴ ┴ ┴ ┴ ┴ ┴ └────┘ ┴ ┴
doc └────┘
141 begin
st └─────
142 cases option.is_some_iff_exists.mp (lookup_is_some.mpr (mem_keys_of_mem h)) with b' h',
id └──────────────────────────┘ └────────────────┘ └─────────────┘ ┴
src └────┘└──────────────────────────┘┴ └────────────────┘┴ └─────────────┘┴ └───────────┘
typ └────┘└──────────────────────────┘┴ └────────────────┘┴ └─────────────┘┴┴└───────────┘
doc └────┘ ┴ ┴ ┴ └───────────┘
txt └────┘ ┴ ┴ ┴ └───────────┘
par └────┘ ┴ ┴ ┴ └───────────┘
pid ┴ ┴ ┴ ┴ └┘└─────────┘
st ───────────────────────────────────────────────────────────────────────────────────────┘└─
143 cases nd.eq_of_mk_mem h (of_mem_lookup h'),
id └─────────────┘ ┴ └───────────┘ └┘
src └────┘└─────────────┘┴ ┴ └───────────┘┴ ┴
typ └────┘└─────────────┘┴┴┴ └───────────┘┴└┘┴
doc └────┘ ┴ ┴ ┴ ┴
txt └────┘ ┴ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴
st ───────────────────────────────────────────┘└─
144 exact h'
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ──────────┘
145 end
st └─┘
146
147 theorem map_lookup_eq_find (a : α) : ∀ l : list (sigma β),
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
148 (lookup a l).map (sigma.mk a) = find (λ s, a = s.1) l
id └────┘ ┴ ┴ └─┘ └──────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴
src └────┘ └─┘ └──────┘ ┴ └──┘ ┴ ┴
typ └────┘ ┴ ┴ └─┘ └──────┘ ┴ ┴ └──┘ ┴ ┴ ┴ ┴┴ ┴
doc └────┘ └──┘
149 | [] := rfl
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
150 | (⟨a', b'⟩ :: l) := begin
id └┘
src └┘
typ └┘
st └─────
151 by_cases h : a = a',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
152 { subst a', simp },
id └┘
src └────┘ └───┘
typ └────┘└┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ───┘└──────┘└─────┘└┘└
153 { simp [h, map_lookup_eq_find] }
id ┴ └────────────────┘
src └────┘ └┘ └┘
typ └────┘┴└┘└────────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ────────────────────────────────┘└─
154 end
st ──┘
155
156 theorem mem_lookup_iff {a : α} {b : β a} {l : list (sigma β)} (nd : l.nodupkeys) :
id ┴ ┴ ┴ └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴└────────┘
157 b ∈ lookup a l ↔ sigma.mk a b ∈ l :=
id ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src ┴ └────┘ ┴ └──────┘ ┴
typ ┴ ┴ └────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └────┘
158 ⟨of_mem_lookup, mem_lookup nd⟩
id └───────────┘ └────────┘ └┘
src └───────────┘ └────────┘
typ └───────────┘ └────────┘ └┘
159
160 theorem perm_lookup (a : α) {l₁ l₂ : list (sigma β)}
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
161 (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) : lookup a l₁ = lookup a l₂ :=
id └┘└────────┘ └┘└────────┘ └┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
src └────────┘ └────────┘ ┴ └────┘ ┴ └────┘
typ └┘└────────┘ └┘└────────┘ └┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
doc ┴ └────┘ └────┘
162 by ext b; simp [mem_lookup_iff, nd₁, nd₂]; exact mem_of_perm p
id └────────────┘ └─┘ └─┘ └─────────┘ ┴
src └───┘ └────┘└────────────┘└┘ └┘ ┴ └────┘└─────────┘┴ └
typ └───┘ └────┘└────────────┘└┘└─┘└┘└─┘┴ └────┘└─────────┘┴┴└
doc └───┘ └────┘ └┘ └┘ ┴ └────┘ ┴ └
txt └───┘ └────┘ └┘ └┘ ┴ └────┘ ┴ └
par └───┘ └────┘ └┘ └┘ ┴ └────┘ ┴ └
pid └┘ ┴┴ └┘ └┘ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────────
163
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
164 lemma mem_ext {l₀ l₁ : list (sigma β)}
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
165 (nd₀ : l₀.nodup) (nd₁ : l₁.nodup)
id └┘└────┘ └┘└────┘
src └────┘ └────┘
typ └┘└────┘ └┘└────┘
doc └────┘ └────┘
166 (h : ∀ x, x ∈ l₀ ↔ x ∈ l₁) : l₀ ~ l₁ :=
id ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └┘
src ┴ ┴ ┴ ┴
typ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └┘ ┴ └┘
doc ┴
167 begin
st └─────
168 induction l₀ with x xs generalizing l₁; cases l₁ with x ys,
id └┘ └┘
src └────────┘ └────────────────────────┘ └────┘ └────────┘
typ └────────┘└┘└────────────────────────┘ └────┘└┘└────────┘
doc └────────┘ └────────────────────────┘ └────┘ └────────┘
txt └────────┘ └────────────────────────┘ └────┘ └────────┘
par └────────┘ └────────────────────────┘ └────┘ └────────┘
pid ┴ ┴└───────┘└──────────────┘ ┴ └────────┘
st ───────────────────────────────────────────────────────────┘└─
169 { constructor },
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴
st ───┘└──────────┘└┘└
170 iterate 2
src └─────────
typ └─────────
doc └─────────
txt └─────────
par └─────────
pid ┴└─
st ────────────
171 { specialize h x, simp at h,
id ┴ ┴
src ───┘└─────────┘ ┴ └┘└───────┘└─
typ ───┘└─────────┘┴┴┴└┘└───────┘└─
doc ───┘└─────────┘ ┴ └┘└───────┘└─
txt ───┘└─────────┘ ┴ └┘└───────┘└─
par ───┘└─────────┘ ┴ └┘└───────┘└─
pid ──────────────┘ ┴ └────────────
st ─────────────────┘└─────────┘└─
172 cases h },
id ┴
src ───┘└────┘ ┴┴
typ ───┘└────┘┴┴┴
doc ───┘└────┘ ┴┴
txt ───┘└────┘ ┴┴
par ───┘└────┘ ┴┴
pid ─────────┘ └┘
st ───────────┘└┘└
173 simp at nd₀ nd₁, rename x y, classical,
src └─────────────┘ └────────┘ └───────┘
typ └─────────────┘ └────────┘ └───────┘
doc └─────────────┘ └────────┘ └───────┘
txt └─────────────┘ └────────┘ └───────┘
par └─────────────┘ └────────┘ └───────┘
pid ┴└────────┘ └┘└┘
st ────────────────┘└──────────┘└─────────┘└─
174 cases nd₀, cases nd₁,
id └─┘ └─┘
src └────┘ └────┘
typ └────┘└─┘ └────┘└─┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴ ┴
st ──────────┘└─────────┘└─
175 by_cases h' : x = y,
id ┴ ┴ ┴
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
176 { subst y, constructor, apply l₀_ih ‹ _ › ‹ nodup ys ›,
id ┴ └───┘ ┴ ┴ └───┘ └┘
src └────┘ └─────────┘ └────┘ ┴┴└─┘┴┴ ┴└───┘┴ ┴
typ └────┘┴ └─────────┘ └────┘└───┘┴┴└─┘┴┴ ┴└───┘┴└┘┴
doc └────┘ └─────────┘ └────┘ ┴┴└─┘┴┴ ┴└───┘┴ ┴
txt └────┘ └─────────┘ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴
par └────┘ └─────────┘ └────┘ ┴ └─┘ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ └─┘ ┴ ┴ ┴ ┴
st ───┘└─────┘└───────────┘└──────────────────────────────┘└─
177 intro a, specialize h a, simp at h,
id ┴ ┴
src └─────┘ └─────────┘ ┴ └───────┘
typ └─────┘ └─────────┘┴┴┴ └───────┘
doc └─────┘ └─────────┘ ┴ └───────┘
txt └─────┘ └─────────┘ ┴ └───────┘
par └─────┘ └─────────┘ ┴ └───────┘
pid └┘ ┴ ┴ ┴└──┘
st ──────────┘└──────────────┘└─────────┘└─
178 by_cases h' : a = x,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────┘└─
179 { subst a, rw ← not_iff_not, split; intro; assumption },
id ┴ └─────────┘
src └────┘ └───┘└─────────┘ └───┘ └───┘ └─────────┘
typ └────┘┴ └───┘└─────────┘ └───┘ └───┘ └─────────┘
doc └────┘ └───┘ └───┘ └───┘ └─────────┘
txt └────┘ └───┘ └───┘ └───┘ └─────────┘
par └────┘ └───┘ └───┘ └───┘ └─────────┘
pid ┴ └─┘ ┴
st ─────┘└─────┘└────────────────┘└─────────────────────────┘└┘└
180 { simp [h'] at h, exact h } },
id └┘ ┴
src └────┘ └────┘ └────┘ ┴
typ └────┘└┘└────┘ └────┘┴┴
doc └────┘ └────┘ └────┘ ┴
txt └────┘ └────┘ └────┘ ┴
par └────┘ └────┘ └────┘ ┴
pid ┴┴ ┴┴└──┘ ┴ ┴
st ───────────────────┘└────────┘└──┘└
181 { transitivity x :: y :: ys.erase x,
id ┴ └──────┘ ┴
src └───────────┘ ┴ ┴ ┴ ┴└──────┘┴
typ └───────────┘ ┴ ┴┴┴ ┴└──────┘┴┴
doc └───────────┘ ┴ ┴ ┴ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────┘└─
182 { constructor, apply l₀_ih ‹ _ ›,
id └───┘
src └─────────┘ └────┘ ┴ └─┘
typ └─────────┘ └────┘└───┘┴ └─┘
doc └─────────┘ └────┘ ┴ └─┘
txt └─────────┘ └────┘ ┴ └─┘
par └─────────┘ └────┘ ┴ └─┘
pid ┴ ┴ └─┘
st ─────┘└─────────┘└─────────────────┘└─
183 { simp, split, { intro, apply nd₁_left, apply mem_of_mem_erase a },
id └──────────────┘ ┴
src └──┘ └───┘ └───┘ └────┘ └────┘└──────────────┘┴ ┴
typ └──┘ └───┘ └───┘ └────┘ └────┘└──────────────┘┴┴┴
doc └──┘ └───┘ └───┘ └────┘ └────┘ ┴ ┴
txt └──┘ └───┘ └───┘ └────┘ └────┘ ┴ ┴
par └──┘ └───┘ └───┘ └────┘ └────┘ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────┘└──┘└─────┘└──┘└───┘└──────────────┘└─────────────────────────┘└┘└
184 apply nodup_erase_of_nodup; assumption },
id └──────────────────┘
src └────┘└──────────────────┘ └─────────┘
typ └────┘└──────────────────┘ └─────────┘
doc └────┘ └─────────┘
txt └────┘ └─────────┘
par └────┘ └─────────┘
pid ┴ ┴
st ──────────────────────────────────────────────┘└┘└
185 { intro a, specialize h a, simp at h,
id ┴ ┴
src └─────┘ └─────────┘ ┴ └───────┘
typ └─────┘ └─────────┘┴┴┴ └───────┘
doc └─────┘ └─────────┘ ┴ └───────┘
txt └─────┘ └─────────┘ ┴ └───────┘
par └─────┘ └─────────┘ ┴ └───────┘
pid └┘ ┴ ┴ ┴└──┘
st ──────────────┘└──────────────┘└─────────┘└─
186 by_cases h' : a = x,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴
typ └───────┘ └─┘┴┴ ┴┴
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────────┘└─
187 { subst a, rw ← not_iff_not, split; intro, simp [mem_erase_of_nodup,*], assumption },
id ┴ └─────────┘ └────────────────┘
src └────┘ └───┘└─────────┘ └───┘ └───┘ └────┘└────────────────┘└─┘ └─────────┘
typ └────┘┴ └───┘└─────────┘ └───┘ └───┘ └────┘└────────────────┘└─┘ └─────────┘
doc └────┘ └───┘ └───┘ └───┘ └────┘ └─┘ └─────────┘
txt └────┘ └───┘ └───┘ └───┘ └────┘ └─┘ └─────────┘
par └────┘ └───┘ └───┘ └───┘ └────┘ └─┘ └─────────┘
pid ┴ └─┘ ┴┴ └─┘ ┴
st ─────────┘└─────┘└────────────────┘└────────────┘└───────────────────────────┘└───────────┘└┘└
188 { simp [h'] at h, simp [h], apply or_congr, refl,
id └┘ ┴ └──────┘
src └────┘ └────┘ └────┘ ┴ └────┘└──────┘ └──┘
typ └────┘└┘└────┘ └────┘┴┴ └────┘└──────┘ └──┘
doc └────┘ └────┘ └────┘ ┴ └────┘ └──┘
txt └────┘ └────┘ └────┘ ┴ └────┘ └──┘
par └────┘ └────┘ └────┘ ┴ └────┘ └──┘
pid ┴┴ ┴┴└──┘ ┴┴ ┴ ┴
st ───────────────────────┘└────────┘└──────────────┘└────┘└─
189 simp [mem_erase_of_ne,*] } } },
id └─────────────┘
src └────┘└─────────────┘└──┘
typ └────┘└─────────────┘└──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴┴ └─┘┴
st ──────────────────────────────────┘└────┘└
190 transitivity y :: x :: ys.erase x,
id ┴ └──────┘ ┴
src └───────────┘ ┴ ┴ ┴ ┴└──────┘┴
typ └───────────┘┴┴ ┴ ┴ ┴└──────┘┴┴
doc └───────────┘ ┴ ┴ ┴ ┴ ┴
txt └───────────┘ ┴ ┴ ┴ ┴ ┴
par └───────────┘ ┴ ┴ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴ ┴ ┴
st ────────────────────────────────────┘└─
191 { constructor },
src └──────────┘
typ └──────────┘
doc └──────────┘
txt └──────────┘
par └──────────┘
pid ┴
st ─────┘└──────────┘└┘└
192 { constructor, symmetry, apply perm_erase,
id └────────┘
src └─────────┘ └──────┘ └────┘└────────┘
typ └─────────┘ └──────┘ └────┘└────────┘
doc └─────────┘ └──────┘ └────┘
txt └─────────┘ └──────┘ └────┘
par └─────────┘ └──────┘ └────┘
pid ┴
st ────────────────┘└────────┘└────────────────┘└─
193 specialize h x, simp [h'] at h, exact h } }
id ┴ ┴ └┘ ┴
src └─────────┘ ┴ └────┘ └────┘ └────┘ ┴
typ └─────────┘┴┴┴ └────┘└┘└────┘ └────┘┴┴
doc └─────────┘ ┴ └────┘ └────┘ └────┘ ┴
txt └─────────┘ ┴ └────┘ └────┘ └────┘ ┴
par └─────────┘ ┴ └────┘ └────┘ └────┘ ┴
pid ┴ ┴ ┴┴ ┴┴└──┘ ┴ ┴
st ───────────────────┘└──────────────┘└────────┘└───
194 end
st ──┘
195
196 lemma lookup_ext {l₀ l₁ : list (sigma β)}
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
197 (nd₀ : l₀.nodupkeys) (nd₁ : l₁.nodupkeys)
id └┘└────────┘ └┘└────────┘
src └────────┘ └────────┘
typ └┘└────────┘ └┘└────────┘
198 (h : ∀ x y, y ∈ l₀.lookup x ↔ y ∈ l₁.lookup x) : l₀ ~ l₁ :=
id ┴ ┴ ┴ ┴ └┘└─────┘ ┴ ┴ ┴ ┴ └┘└─────┘ ┴ └┘ ┴ └┘
src ┴ └─────┘ ┴ ┴ └─────┘ ┴
typ ┴ ┴ ┴ ┴ └┘└─────┘ ┴ ┴ ┴ ┴ └┘└─────┘ ┴ └┘ ┴ └┘
doc └─────┘ └─────┘ ┴
199 mem_ext (nodup_of_nodupkeys nd₀) (nodup_of_nodupkeys nd₁)
id └─────┘ └────────────────┘ └─┘ └────────────────┘ └─┘
src └─────┘ └────────────────┘ └────────────────┘
typ └─────┘ └────────────────┘ └─┘ └────────────────┘ └─┘
200 (λ ⟨a,b⟩, by rw [← mem_lookup_iff, ← mem_lookup_iff, h]; assumption)
id ┴ └────────────┘ └────────────┘ ┴
src └────┘└────────────┘└──┘└────────────┘└┘ ┴ └────────┘
typ ┴ └────┘└────────────┘└──┘└────────────┘└┘┴┴ └────────┘
doc └────┘ └──┘ └┘ ┴ └────────┘
txt └────┘ └──┘ └┘ ┴ └────────┘
par └────┘ └──┘ └┘ ┴ └────────┘
pid └──┘ └──┘ └┘ ┴
st └───────────────────┘└────────────────┘└─┘┴└──────────┘
201
202 /- lookup_all -/
203
204 /-- `lookup_all a l` is the list of all values in `l` corresponding to the key `a`. -/
205 def lookup_all (a : α) : list (sigma β) → list (β a)
id ┴ └──┘ └───┘ ┴ ┴ └──┘ ┴ ┴
src └──┘ └───┘ └──┘
typ ┴ └──┘ └───┘ ┴ ┴ └──┘ ┴ ┴
206 | [] := []
id └┘ └┘
src └┘ └┘
typ └┘ └┘
207 | (⟨a', b⟩ :: l) := if h : a' = a then eq.rec_on h b :: lookup_all l else lookup_all l
id └┘ ┴ └┘ ┴ └┘ ┴ ┴ └───────┘ ┴ └┘ └────────┘ └────────┘
src └┘ └┘ ┴ └───────┘ └┘
typ └┘ ┴ └┘ ┴ └┘ ┴ ┴ └───────┘ ┴ └┘ └────────┘ └────────┘
208
209 @[simp] theorem lookup_all_nil (a : α) : lookup_all a [] = @nil (β a) := rfl
id ┴ └────────┘ ┴ └┘ ┴ └─┘ ┴ ┴ └─┘
src └────────┘ └┘ ┴ └─┘ └─┘
typ ┴ └────────┘ ┴ └┘ ┴ └─┘ ┴ ┴ └─┘
doc └──┘ └────────┘
210
211 @[simp] theorem lookup_all_cons_eq (l) (a : α) (b : β a) :
id ┴ ┴ ┴
typ ┴ ┴ ┴
doc └──┘
212 lookup_all a (⟨a, b⟩::l) = b :: lookup_all a l :=
id └────────┘ ┴ ┴ ┴ └┘┴ ┴ ┴ └┘ └────────┘ ┴ ┴
src └────────┘ └┘ ┴ └┘ └────────┘
typ └────────┘ ┴ ┴ ┴ └┘┴ ┴ ┴ └┘ └────────┘ ┴ ┴
doc └────────┘ └────────┘
213 dif_pos rfl
id └─────┘ └─┘
src └─────┘ └─┘
typ └─────┘ └─┘
214
215 @[simp] theorem lookup_all_cons_ne (l) {a} :
doc └──┘
216 ∀ s : sigma β, a ≠ s.1 → lookup_all a (s::l) = lookup_all a l
id ┴ └───┘ ┴ ┴ ┴ ┴┴ └────────┘ ┴ ┴└┘┴ ┴ └────────┘ ┴ ┴
src └───┘ ┴ ┴ └────────┘ └┘ ┴ └────────┘
typ ┴ └───┘ ┴ ┴ ┴ ┴┴ └────────┘ ┴ ┴└┘┴ ┴ └────────┘ ┴ ┴
doc └────────┘ └────────┘
217 | ⟨a', b⟩ h := dif_neg h.symm
id ┴ └─────┘ └───┘
src └─────┘ └───┘
typ ┴ └─────┘ └───┘
218
219 theorem lookup_all_eq_nil {a : α} : ∀ {l : list (sigma β)},
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
220 lookup_all a l = [] ↔ ∀ b : β a, sigma.mk a b ∉ l
id └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └────────┘ ┴ └┘ ┴ └──────┘ ┴
typ └────────┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └────────┘
221 | [] := by simp
id └┘
src └┘ └───┘
typ └┘ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
222 | (⟨a', b⟩ :: l) := begin
id └┘
src └┘
typ └┘
st └─────
223 by_cases h : a = a',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ────────────────────┘└─
224 { subst a', simp, exact λ H, H b (or.inl rfl) },
id └┘ ┴ └────┘ └─┘
src └────┘ └──┘ └────┘ └──┘ ┴ ┴ └────┘┴└─┘└┘
typ └────┘└┘ └──┘ └────┘ └──┘ ┴┴┴ └────┘┴└─┘└┘
doc └────┘ └──┘ └────┘ └──┘ ┴ ┴ ┴ └┘
txt └────┘ └──┘ └────┘ └──┘ ┴ ┴ ┴ └┘
par └────┘ └──┘ └────┘ └──┘ ┴ ┴ ┴ └┘
pid ┴ ┴ └──┘ ┴ ┴ ┴ ┴┴
st ───┘└──────┘└────┘└────────────────────────────┘└┘└
225 { simp [h, lookup_all_eq_nil] },
id ┴
src └────┘ └┘ └┘
typ └────┘┴└┘└───────────────┘└┘
doc └────┘ └┘ └┘
txt └────┘ └┘ └┘
par └────┘ └┘ └┘
pid ┴┴ └┘ ┴┴
st ───────────────────────────────┘└──
226 end
st ──┘
227
228 theorem head_lookup_all (a : α) : ∀ l : list (sigma β),
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
229 head' (lookup_all a l) = lookup a l
id └───┘ └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴
src └───┘ └────────┘ ┴ └────┘
typ └───┘ └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴
doc └────────┘ └────┘
230 | [] := by simp
id └┘
src └┘ └───┘
typ └┘ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
231 | (⟨a', b⟩ :: l) := by by_cases h : a = a'; [{subst h, simp}, simp *]
id └┘ ┴ ┴ └┘ ┴ ┴
src └┘ └───────┘ └─┘ ┴┴┴ ┴ └────┘ └──┘ └────┘
typ └┘ └───────┘ └─┘┴┴┴┴└┘ ┴ └────┘┴ └──┘ └────┘
doc └───────┘ └─┘ ┴ ┴ └────┘ └──┘ └────┘
txt └───────┘ └─┘ ┴ ┴ └────┘ └──┘ └────┘
par └───────┘ └─┘ ┴ ┴ └────┘ └──┘ └────┘
pid ┴ └─┘ ┴ ┴ ┴ ┴┴
st └─────────────────────┘└──────┘└────┘└┘└──────┘
232
233 theorem mem_lookup_all {a : α} {b : β a} :
id ┴ ┴ ┴
typ ┴ ┴ ┴
234 ∀ {l : list (sigma β)}, b ∈ lookup_all a l ↔ sigma.mk a b ∈ l
id ┴ └──┘ └───┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
src └──┘ └───┘ ┴ └────────┘ ┴ └──────┘ ┴
typ ┴ └──┘ └───┘ ┴ ┴ ┴ └────────┘ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴
doc └────────┘
235 | [] := by simp
id └┘
src └┘ └───┘
typ └┘ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
236 | (⟨a', b'⟩ :: l) := by by_cases h : a = a'; [{subst h, simp *}, simp *]
id └┘ ┴ ┴ └┘ ┴ ┴
src └┘ └───────┘ └─┘ ┴┴┴ ┴ └────┘ └────┘ └────┘
typ └┘ └───────┘ └─┘┴┴┴┴└┘ ┴ └────┘┴ └────┘ └────┘
doc └───────┘ └─┘ ┴ ┴ └────┘ └────┘ └────┘
txt └───────┘ └─┘ ┴ ┴ └────┘ └────┘ └────┘
par └───────┘ └─┘ ┴ ┴ └────┘ └────┘ └────┘
pid ┴ └─┘ ┴ ┴ ┴ ┴┴ ┴┴
st └─────────────────────┘└──────┘└──────┘└┘└──────┘
237
238 theorem lookup_all_sublist (a : α) :
id ┴
typ ┴
239 ∀ l : list (sigma β), (lookup_all a l).map (sigma.mk a) <+ l
id ┴ └──┘ └───┘ ┴ └────────┘ ┴ ┴ └─┘ └──────┘ ┴ └┘ ┴
src └──┘ └───┘ └────────┘ └─┘ └──────┘ └┘
typ ┴ └──┘ └───┘ ┴ └────────┘ ┴ ┴ └─┘ └──────┘ ┴ └┘ ┴
doc └────────┘
240 | [] := by simp
id └┘
src └┘ └───┘
typ └┘ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st └────┘
241 | (⟨a', b'⟩ :: l) := begin
id └┘
src └┘
typ └┘
st └─────
242 by_cases h : a = a',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ──────────────────────┘└─
243 { subst h, simp, exact (lookup_all_sublist l).cons2 _ _ _ },
id ┴ └────────────────┘ ┴
src └────┘ └──┘ └────┘ ┴ └────────────┘
typ └────┘┴ └──┘ └────┘ └────────────────┘┴┴└────────────┘
doc └────┘ └──┘ └────┘ ┴ └────────────┘
txt └────┘ └──┘ └────┘ ┴ └────────────┘
par └────┘ └──┘ └────┘ ┴ └────────────┘
pid ┴ ┴ ┴ └───────────┘┴
st ─────┘└─────┘└────┘└─────────────────────────────────────────┘└┘└
244 { simp [h], exact (lookup_all_sublist l).cons _ _ _ }
id ┴ └────────────────┘ ┴
src └────┘ ┴ └────┘ ┴ └───────────┘
typ └────┘┴┴ └────┘ └────────────────┘┴┴└───────────┘
doc └────┘ ┴ └────┘ ┴ └───────────┘
txt └────┘ ┴ └────┘ ┴ └───────────┘
par └────┘ ┴ └────┘ ┴ └───────────┘
pid ┴┴ ┴ ┴ ┴ └──────────┘┴
st ─────────────┘└────────────────────────────────────────┘└─
245 end
st ────┘
246
247 theorem lookup_all_length_le_one (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
id ┴ └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ ┴ └──┘ └───┘ ┴ ┴└────────┘
248 length (lookup_all a l) ≤ 1 :=
id └────┘ └────────┘ ┴ ┴ ┴
src └────┘ └────────┘ ┴
typ └────┘ └────────┘ ┴ ┴ ┴
doc └────────┘
249 by have := nodup_of_sublist (map_sublist_map _ $ lookup_all_sublist a l) h;
id └──────────────┘ └─────────────┘ └────────────────┘ ┴ ┴ ┴
src └──────┘└──────────────┘┴ └─────────────┘└─┘ ┴└────────────────┘┴ ┴ └┘
typ └──────┘└──────────────┘┴ └─────────────┘└─┘ ┴└────────────────┘┴┴┴┴└┘┴
doc └──────┘ ┴ └─┘ ┴ ┴ ┴ └┘
txt └──────┘ ┴ └─┘ ┴ ┴ ┴ └┘
par └──────┘ ┴ └─┘ ┴ ┴ ┴ └┘
pid └───┘└─┘ ┴ └─┘ ┴ ┴ ┴ └┘
st └─────────────────────────────────────────────────────────────────────────
250 rw map_map at this; rwa [← nodup_repeat, ← map_const _ a]
id └─────┘ └──────────┘ └───────┘ ┴
src └─┘└─────┘└──────┘ └─────┘└──────────┘└──┘└───────┘└─┘ └─
typ └─┘└─────┘└──────┘ └─────┘└──────────┘└──┘└───────┘└─┘┴└─
doc └─┘ └──────┘ └─────┘ └──┘ └─┘ └─
txt └─┘ └──────┘ └─────┘ └──┘ └─┘ └─
par └─┘ └──────┘ └─────┘ └──┘ └─┘ └─
pid ┴ └──────┘ └──┘ └──┘ └─┘ ┴└
st ─────┘└─────┘└─────────────┘└────────────┘└───────────────┘┴└
251
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
252 theorem lookup_all_eq_lookup (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
id ┴ └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ ┴ └──┘ └───┘ ┴ ┴└────────┘
253 lookup_all a l = (lookup a l).to_list :=
id └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘
src └────────┘ ┴ └────┘ └─────┘
typ └────────┘ ┴ ┴ ┴ └────┘ ┴ ┴ └─────┘
doc └────────┘ └────┘
254 begin
st └─────
255 rw ← head_lookup_all,
id └─────────────┘
src └───┘└─────────────┘
typ └───┘└─────────────┘
doc └───┘
txt └───┘
par └───┘
pid └─┘
st ─────────────────────┘└─
256 have := lookup_all_length_le_one a h, revert this,
id └──────────────────────┘ ┴ ┴
src └──────┘└──────────────────────┘┴ ┴ └─────────┘
typ └──────┘└──────────────────────┘┴┴┴┴ └─────────┘
doc └──────┘ ┴ ┴ └─────────┘
txt └──────┘ ┴ ┴ └─────────┘
par └──────┘ ┴ ┴ └─────────┘
pid └───┘└─┘ ┴ ┴ └───┘
st ─────────────────────────────────────┘└───────────┘└─
257 rcases lookup_all a l with _|⟨b, _|⟨c, l⟩⟩; intro; try {refl},
id └────────┘ ┴ ┴
src └─────┘└────────┘┴ ┴ └───────────────────┘ └───┘ └───┘└──┘┴
typ └─────┘└────────┘┴┴┴┴└───────────────────┘ └───┘ └───┘└──┘┴
doc └─────┘└────────┘┴ ┴ └───────────────────┘ └───┘ └───┘└──┘┴
txt └─────┘ ┴ ┴ └───────────────────┘ └───┘ └───┘└──┘┴
par └─────┘ ┴ ┴ └───────────────────┘ └───┘ └───┘└──┘┴
pid ┴ ┴ ┴ └───────────────────┘ └─────┘
st ─────────────────────────────────────────────────────────┘└──┘└┘└
258 exact absurd this dec_trivial
id └────┘ └──┘ └─────────┘
src └────┘└────┘┴ ┴└─────────┘┴
typ └────┘└────┘┴└──┘┴└─────────┘┴
doc └────┘ ┴ ┴└─────────┘┴
txt └────┘ ┴ ┴ ┴
par └────┘ ┴ ┴ ┴
pid ┴ ┴ ┴ ┴
st ───────────────────────────────┘
259 end
st └─┘
260
261 theorem lookup_all_nodup (a : α) {l : list (sigma β)} (h : l.nodupkeys) :
id ┴ └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ ┴ └──┘ └───┘ ┴ ┴└────────┘
262 (lookup_all a l).nodup :=
id └────────┘ ┴ ┴ └───┘
src └────────┘ └───┘
typ └────────┘ ┴ ┴ └───┘
doc └────────┘ └───┘
263 by rw lookup_all_eq_lookup a h; apply option.to_list_nodup
id └──────────────────┘ ┴ ┴ └──────────────────┘
src └─┘└──────────────────┘┴ ┴ └────┘└──────────────────┘└
typ └─┘└──────────────────┘┴┴┴┴ └────┘└──────────────────┘└
doc └─┘ ┴ ┴ └────┘ └
txt └─┘ ┴ ┴ └────┘ └
par └─┘ ┴ ┴ └────┘ └
pid ┴ ┴ ┴ ┴ └
st └────────────────────────────────────────────────────────
264
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
265 theorem perm_lookup_all (a : α) {l₁ l₂ : list (sigma β)}
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
266 (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) (p : l₁ ~ l₂) : lookup_all a l₁ = lookup_all a l₂ :=
id └┘└────────┘ └┘└────────┘ └┘ ┴ └┘ └────────┘ ┴ └┘ ┴ └────────┘ ┴ └┘
src └────────┘ └────────┘ ┴ └────────┘ ┴ └────────┘
typ └┘└────────┘ └┘└────────┘ └┘ ┴ └┘ └────────┘ ┴ └┘ ┴ └────────┘ ┴ └┘
doc ┴ └────────┘ └────────┘
267 by simp [lookup_all_eq_lookup, nd₁, nd₂, perm_lookup a nd₁ nd₂ p]
id └──────────────────┘ └─┘ └─┘ └─────────┘ ┴ └─┘ └─┘ ┴
src └────┘└──────────────────┘└┘ └┘ └┘└─────────┘┴ ┴ ┴ ┴ └─
typ └────┘└──────────────────┘└┘└─┘└┘└─┘└┘└─────────┘┴┴┴└─┘┴└─┘┴┴└─
doc └────┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴ └─
txt └────┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴ └─
par └────┘ └┘ └┘ └┘ ┴ ┴ ┴ ┴ └─
pid ┴┴ └┘ └┘ └┘ ┴ ┴ ┴ ┴ ┴└
st └───────────────────────────────────────────────────────────────
268
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
269 /- kreplace -/
src ───────────────
typ ───────────────
doc ───────────────
txt ───────────────
par ───────────────
pid ───────────────
st ───────────────
270
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
271 def kreplace (a : α) (b : β a) : list (sigma β) → list (sigma β) :=
id ┴ ┴ ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
src └──┘ └───┘ └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
272 lookmap $ λ s, if h : a = s.1 then some ⟨a, b⟩ else none
id └─────┘ ┴ └┘ ┴ ┴ ┴┴ └──┘ ┴ ┴ └──┘
src └─────┘ └┘ ┴ ┴ └──┘ └──┘
typ └─────┘ ┴ └┘ ┴ ┴ ┴┴ └──┘ ┴ ┴ └──┘
doc └─────┘
273
274 theorem kreplace_of_forall_not (a : α) (b : β a) {l : list (sigma β)}
id ┴ ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴
275 (H : ∀ b : β a, sigma.mk a b ∉ l) : kreplace a b l = l :=
id ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └──────┘ ┴ └──────┘ ┴
typ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
276 lookmap_of_forall_not _ $ begin
id └───────────────────┘
src └───────────────────┘
typ └───────────────────┘
st └─────
277 rintro ⟨a', b'⟩ h, dsimp, split_ifs,
src └───────────────┘ └───┘ └───────┘
typ └───────────────┘ └───┘ └───────┘
doc └───────────────┘ └───┘ └───────┘
txt └───────────────┘ └───┘ └───────┘
par └───────────────┘ └───┘ └───────┘
pid └─────────┘
st ──────────────────┘└─────┘└─────────┘└─
278 { subst a', exact H _ h }, {refl}
id └┘ ┴ ┴
src └────┘ └────┘ └─┘ ┴ └──┘
typ └────┘└┘ └────┘┴└─┘┴┴ └──┘
doc └────┘ └────┘ └─┘ ┴ └──┘
txt └────┘ └────┘ └─┘ ┴ └──┘
par └────┘ └────┘ └─┘ ┴ └──┘
pid ┴ ┴ └─┘ ┴
st ───┘└──────┘└────────────┘└┘└────┘└─
279 end
st ──┘
280
281 theorem kreplace_self {a : α} {b : β a} {l : list (sigma β)}
id ┴ ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴
282 (nd : nodupkeys l) (h : sigma.mk a b ∈ l) : kreplace a b l = l :=
id └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
src └───────┘ └──────┘ ┴ └──────┘ ┴
typ └───────┘ ┴ └──────┘ ┴ ┴ ┴ ┴ └──────┘ ┴ ┴ ┴ ┴ ┴
283 begin
st └─────
284 refine (lookmap_congr _).trans
id └───────────┘
src └─────┘ └───────────┘└─────────
typ └─────┘ └───────────┘└─────────
doc └─────┘ └─────────
txt └─────┘ └─────────
par └─────┘ └─────────
pid ┴ └─────────
st ─────────────────────────────────
285 (lookmap_id' (option.guard (λ s, a = s.1)) _ _),
id └─────────┘ └──────────┘ ┴ ┴
src ───┘ └─────────┘┴ └──────────┘┴ └──┘ ┴┴┴ └───────┘
typ ───┘ └─────────┘┴ └──────────┘┴ └──┘┴┴┴┴ └───────┘
doc ───┘ ┴ └──────────┘┴ └──┘ ┴ ┴ └───────┘
txt ───┘ ┴ ┴ └──┘ ┴ ┴ └───────┘
par ───┘ ┴ ┴ └──┘ ┴ ┴ └───────┘
pid ───┘ ┴ ┴ └──┘ ┴ ┴ └───────┘
st ──────────────────────────────────────────────────┘└─
286 { rintro ⟨a', b'⟩ h', dsimp [option.guard], split_ifs,
id └──────────┘
src └────────────────┘ └─────┘└──────────┘┴ └───────┘
typ └────────────────┘ └─────┘└──────────┘┴ └───────┘
doc └────────────────┘ └─────┘└──────────┘┴ └───────┘
txt └────────────────┘ └─────┘ ┴ └───────┘
par └────────────────┘ └─────┘ ┴ └───────┘
pid └──────────┘ ┴┴ ┴
st ───┘└────────────────┘└────────────────────┘└─────────┘└─
287 { subst a', exact ⟨rfl, heq_of_eq $ nd.eq_of_mk_mem h h'⟩ },
id └┘ └─┘ └───────┘ └─────────────┘ ┴ └┘
src └────┘ └────┘ └─┘└┘└───────┘┴ ┴└─────────────┘┴ ┴ └┘
typ └────┘└┘ └────┘ └─┘└┘└───────┘┴ ┴└─────────────┘┴┴┴└┘└┘
doc └────┘ └────┘ └┘ ┴ ┴ ┴ ┴ └┘
txt └────┘ └────┘ └┘ ┴ ┴ ┴ ┴ └┘
par └────┘ └────┘ └┘ ┴ ┴ ┴ ┴ └┘
pid ┴ ┴ └┘ ┴ ┴ ┴ ┴ ┴┴
st ─────┘└──────┘└──────────────────────────────────────────────┘└┘└
288 { refl } },
src └───┘
typ └───┘
doc └───┘
txt └───┘
par └───┘
pid ┴
st ──────────┘└──┘└
289 { rintro ⟨a₁, b₁⟩ ⟨a₂, b₂⟩, dsimp [option.guard], split_ifs,
id └──────────┘
src └──────────────────────┘ └─────┘└──────────┘┴ └───────┘
typ └──────────────────────┘ └─────┘└──────────┘┴ └───────┘
doc └──────────────────────┘ └─────┘└──────────┘┴ └───────┘
txt └──────────────────────┘ └─────┘ ┴ └───────┘
par └──────────────────────┘ └─────┘ ┴ └───────┘
pid └────────────────┘ ┴┴ ┴
st ───────────────────────────┘└────────────────────┘└─────────┘└─
290 { subst a₁, rintro ⟨⟩, simp }, { rintro ⟨⟩ } },
id └┘
src └────┘ └───────┘ └───┘ └────────┘
typ └────┘└┘ └───────┘ └───┘ └────────┘
doc └────┘ └───────┘ └───┘ └────────┘
txt └────┘ └───────┘ └───┘ └────────┘
par └────┘ └───────┘ └───┘ └────────┘
pid ┴ └─┘ ┴ └─┘┴
st ─────┘└──────┘└─────────┘└─────┘└┘└───────────┘└────
291 end
st ──┘
292
293 theorem keys_kreplace (a : α) (b : β a) : ∀ l : list (sigma β),
id ┴ ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴
294 (kreplace a b l).keys = l.keys :=
id └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘
src └──────┘ └──┘ ┴ └───┘
typ └──────┘ ┴ ┴ ┴ └──┘ ┴ ┴└───┘
doc └──┘ └───┘
295 lookmap_map_eq _ _ $ by rintro ⟨a₁, b₂⟩ ⟨a₂, b₂⟩;
id └────────────┘
src └────────────┘ └──────────────────────┘
typ └────────────┘ └──────────────────────┘
doc └──────────────────────┘
txt └──────────────────────┘
par └──────────────────────┘
pid └────────────────┘
st └──────────────────────────
296 dsimp; split_ifs; simp [h] {contextual := tt}
id ┴ └┘
src └───┘ └───────┘ └────┘ └┘ └────────────┘└┘└─
typ └───┘ └───────┘ └────┘┴└┘ └────────────┘└┘└─
doc └───┘ └───────┘ └────┘ └┘ └────────────┘ └─
txt └───┘ └───────┘ └────┘ └┘ └────────────┘ └─
par └───┘ └───────┘ └────┘ └┘ └────────────┘ └─
pid ┴┴ ┴┴ └────────────┘ ┴└
st ────────────────────────────────────────────────
297
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
298 theorem kreplace_nodupkeys (a : α) (b : β a) {l : list (sigma β)} :
id ┴ ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴
299 (kreplace a b l).nodupkeys ↔ l.nodupkeys :=
id └──────┘ ┴ ┴ ┴ └───────┘ ┴ ┴└────────┘
src └──────┘ └───────┘ ┴ └────────┘
typ └──────┘ ┴ ┴ ┴ └───────┘ ┴ ┴└────────┘
300 by simp [nodupkeys, keys_kreplace]
id └───────┘ └───────────┘
src └────┘└───────┘└┘└───────────┘└─
typ └────┘└───────┘└┘└───────────┘└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────────────────────────
301
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
302 theorem perm_kreplace {a : α} {b : β a} {l₁ l₂ : list (sigma β)}
id ┴ ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴
303 (nd : l₁.nodupkeys) : l₁ ~ l₂ →
id └┘└────────┘ └┘ ┴ └┘
src └────────┘ ┴
typ └┘└────────┘ └┘ ┴ └┘
doc ┴
304 kreplace a b l₁ ~ kreplace a b l₂ :=
id └──────┘ ┴ ┴ └┘ ┴ └──────┘ ┴ ┴ └┘
src └──────┘ ┴ └──────┘
typ └──────┘ ┴ ┴ └┘ ┴ └──────┘ ┴ ┴ └┘
doc ┴
305 perm_lookmap _ $ begin
id └──────────┘
src └──────────┘
typ └──────────┘
st └─────
306 refine (nodupkeys_iff_pairwise.1 nd).imp _,
id └────────────────────┘ └┘
src └─────┘ └────────────────────┘└─┘ └─────┘
typ └─────┘ └────────────────────┘└─┘└┘└─────┘
doc └─────┘ └─┘ └─────┘
txt └─────┘ └─┘ └─────┘
par └─────┘ └─┘ └─────┘
pid ┴ └─┘ └─────┘
st ───────────────────────────────────────────┘└─
307 intros x y h z h₁ w h₂,
src └────────────────────┘
typ └────────────────────┘
doc └────────────────────┘
txt └────────────────────┘
par └────────────────────┘
pid └──────────────┘
st ───────────────────────┘└─
308 split_ifs at h₁ h₂; cases h₁; cases h₂,
id └┘ └┘
src └────────────────┘ └────┘ └────┘
typ └────────────────┘ └────┘└┘ └────┘└┘
doc └────────────────┘ └────┘ └────┘
txt └────────────────┘ └────┘ └────┘
par └────────────────┘ └────┘ └────┘
pid └───────┘ ┴ ┴
st ───────────────────────────────────────┘└─
309 exact (h (h_2.symm.trans h_1)).elim
id ┴ └────────────┘ └─┘
src └────┘ ┴ └────────────┘┴ └──────┘
typ └────┘ ┴┴ └────────────┘┴└─┘└──────┘
doc └────┘ ┴ ┴ └──────┘
txt └────┘ ┴ ┴ └──────┘
par └────┘ ┴ ┴ └──────┘
pid ┴ ┴ ┴ └────┘└┘
st ─────────────────────────────────────┘
310 end
st └─┘
311
312 /- kerase -/
313
314 /-- Remove the first pair with the key `a`. -/
315 def kerase (a : α) : list (sigma β) → list (sigma β) :=
id ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
src └──┘ └───┘ └──┘ └───┘
typ ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
316 erasep $ λ s, a = s.1
id └────┘ ┴ ┴ ┴ ┴┴
src └────┘ ┴ ┴
typ └────┘ ┴ ┴ ┴ ┴┴
317
318 @[simp] theorem kerase_nil {a} : @kerase _ β _ a [] = [] :=
id └────┘ ┴ ┴ └┘ ┴ └┘
src └────┘ └┘ ┴ └┘
typ └────┘ ┴ ┴ └┘ ┴ └┘
doc └──┘ └────┘
319 rfl
id └─┘
src └─┘
typ └─┘
320
321 @[simp] theorem kerase_cons_eq {a} {s : sigma β} {l : list (sigma β)} (h : a = s.1) :
id └───┘ ┴ └──┘ └───┘ ┴ ┴ ┴ ┴┴
src └───┘ └──┘ └───┘ ┴ ┴
typ └───┘ ┴ └──┘ └───┘ ┴ ┴ ┴ ┴┴
doc └──┘
322 kerase a (s :: l) = l :=
id └────┘ ┴ ┴ └┘ ┴ ┴ ┴
src └────┘ └┘ ┴
typ └────┘ ┴ ┴ └┘ ┴ ┴ ┴
doc └────┘
323 by simp [kerase, h]
id └────┘ ┴
src └────┘└────┘└┘ └─
typ └────┘└────┘└┘┴└─
doc └────┘└────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────
324
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
325 @[simp] theorem kerase_cons_ne {a} {s : sigma β} {l : list (sigma β)} (h : a ≠ s.1) :
id └───┘ ┴ └──┘ └───┘ ┴ ┴ ┴ ┴┴
src └───┘ └──┘ └───┘ ┴ ┴
typ └───┘ ┴ └──┘ └───┘ ┴ ┴ ┴ ┴┴
doc └──┘
326 kerase a (s :: l) = s :: kerase a l :=
id └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └────┘ ┴ ┴
src └────┘ └┘ ┴ └┘ └────┘
typ └────┘ ┴ ┴ └┘ ┴ ┴ ┴ └┘ └────┘ ┴ ┴
doc └────┘ └────┘
327 by simp [kerase, h]
id └────┘ ┴
src └────┘└────┘└┘ └─
typ └────┘└────┘└┘┴└─
doc └────┘└────┘└┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └─────────────────
328
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
329 @[simp] theorem kerase_of_not_mem_keys {a} {l : list (sigma β)} (h : a ∉ l.keys) :
id └──┘ └───┘ ┴ ┴ ┴ ┴└───┘
src └──┘ └───┘ ┴ └───┘
typ └──┘ └───┘ ┴ ┴ ┴ ┴└───┘
doc └──┘ └───┘
330 kerase a l = l :=
id └────┘ ┴ ┴ ┴ ┴
src └────┘ ┴
typ └────┘ ┴ ┴ ┴ ┴
doc └────┘
331 by induction l with _ _ ih;
id ┴
src └────────┘ └──────────┘
typ └────────┘┴└──────────┘
doc └────────┘ └──────────┘
txt └────────┘ └──────────┘
par └────────┘ └──────────┘
pid ┴ ┴└─────────┘
st └─────────────────────────
332 [refl, { simp [not_or_distrib] at h, simp [h.1, ih h.2] }]
id ┴ └────────────┘ ┴ └┘ ┴
src ┴└──┘ └────┘└────────────┘└────┘ └────┘ └──┘ ┴ └──┘
typ ┴└──┘ └────┘└────────────┘└────┘ └────┘┴└──┘└┘┴┴└──┘
doc └──┘ └────┘ └────┘ └────┘ └──┘ ┴ └──┘
txt └──┘ └────┘ └────┘ └────┘ └──┘ ┴ └──┘
par └──┘ └────┘ └────┘ └────┘ └──┘ ┴ └──┘
pid ┴┴ ┴┴└──┘ ┴┴ └──┘ ┴ └─┘┴
st ─────────┘└──────────────────────────┘└───────────────────┘└┘
333
334 theorem kerase_sublist (a : α) (l : list (sigma β)) : kerase a l <+ l :=
id ┴ └──┘ └───┘ ┴ └────┘ ┴ ┴ └┘ ┴
src └──┘ └───┘ └────┘ └┘
typ ┴ └──┘ └───┘ ┴ └────┘ ┴ ┴ └┘ ┴
doc └────┘
335 erasep_sublist _
id └────────────┘
src └────────────┘
typ └────────────┘
336
337 theorem kerase_keys_subset (a) (l : list (sigma β)) :
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
338 (kerase a l).keys ⊆ l.keys :=
id └────┘ ┴ ┴ └──┘ ┴ ┴└───┘
src └────┘ └──┘ ┴ └───┘
typ └────┘ ┴ ┴ └──┘ ┴ ┴└───┘
doc └────┘ └──┘ └───┘
339 subset_of_sublist (map_sublist_map _ (kerase_sublist a l))
id └───────────────┘ └─────────────┘ └────────────┘ ┴ ┴
src └───────────────┘ └─────────────┘ └────────────┘
typ └───────────────┘ └─────────────┘ └────────────┘ ┴ ┴
340
341 theorem mem_keys_of_mem_keys_kerase {a₁ a₂} {l : list (sigma β)} :
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
342 a₁ ∈ (kerase a₂ l).keys → a₁ ∈ l.keys :=
id └┘ ┴ └────┘ └┘ ┴ └──┘ └┘ ┴ ┴└───┘
src ┴ └────┘ └──┘ ┴ └───┘
typ └┘ ┴ └────┘ └┘ ┴ └──┘ └┘ ┴ ┴└───┘
doc └────┘ └──┘ └───┘
343 @kerase_keys_subset _ _ _ _ _ _
id └────────────────┘
src └────────────────┘
typ └────────────────┘
344
345 theorem exists_of_kerase {a : α} {l : list (sigma β)} (h : a ∈ l.keys) :
id ┴ └──┘ └───┘ ┴ ┴ ┴ ┴└───┘
src └──┘ └───┘ ┴ └───┘
typ ┴ └──┘ └───┘ ┴ ┴ ┴ ┴└───┘
doc └───┘
346 ∃ (b : β a) (l₁ l₂ : list (sigma β)),
id ┴ ┴ ┴ └──┘ └───┘ ┴ ┴
src ┴ └──┘ └───┘ ┴
typ ┴ ┴ ┴ └──┘ └───┘ ┴ ┴
347 a ∉ l₁.keys ∧
id ┴ ┴ └┘└───┘ ┴
src ┴ └───┘ ┴
typ ┴ ┴ └┘└───┘ ┴
doc └───┘
348 l = l₁ ++ ⟨a, b⟩ :: l₂ ∧
id ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴
src ┴ └┘ └┘ ┴
typ ┴ ┴ └┘ └┘ ┴ ┴ └┘ └┘ ┴
349 kerase a l = l₁ ++ l₂ :=
id └────┘ ┴ ┴ ┴ └┘ └┘ └┘
src └────┘ ┴ └┘
typ └────┘ ┴ ┴ ┴ └┘ └┘ └┘
doc └────┘
350 begin
st └─────
351 induction l,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────┘└─
352 case list.nil { cases h },
id ┴
src └──────────────┘└────┘ ┴┴
typ └──────────────┘└────┘┴┴┴
doc └──────────────┘└────┘ ┴┴
txt └──────────────┘└────┘ ┴┴
par └──────────────┘└────┘ ┴┴
pid └───────┘┴└──────┘ └┘
st ────────────────┘└───────┘└┘└
353 case list.cons : hd tl ih {
src └───────────────────────────
typ └───────────────────────────
doc └───────────────────────────
txt └───────────────────────────
par └───────────────────────────
pid └────────┘└─────────┘└──
st ────────────────────────────┘└
354 by_cases e : a = hd.1,
id ┴ ┴ └┘
src ───┘└───────┘ └─┘ ┴┴┴ └┘└─
typ ───┘└───────┘ └─┘┴┴┴┴└┘└┘└─
doc ───┘└───────┘ └─┘ ┴ ┴ └┘└─
txt ───┘└───────┘ └─┘ ┴ ┴ └┘└─
par ───┘└───────┘ └─┘ ┴ ┴ └┘└─
pid ────────────┘ └─┘ ┴ ┴ └───
st ────────────────────────┘└─
355 { subst e,
id ┴
src ─────┘└────┘ └─
typ ─────┘└────┘┴└─
doc ─────┘└────┘ └─
txt ─────┘└────┘ └─
par ─────┘└────┘ └─
pid ───────────┘ └─
st ────┘└──────┘└─
356 exact ⟨hd.2, [], tl, by simp, by cases hd; refl, by simp⟩ },
id └┘ └┘ └┘
src ─────┘└────┘ └──┘ └┘ └┘ ┴└──┘└┘ ┴└────┘ └┘└──┘└┘ ┴└──┘└┘└──
typ ─────┘└────┘ └┘└──┘ └┘└┘└┘ ┴└──┘└┘ ┴└────┘└┘└┘└──┘└┘ ┴└──┘└┘└──
doc ─────┘└────┘ └──┘ └┘ └┘ ┴└──┘└┘ ┴└────┘ └┘└──┘└┘ ┴└──┘└┘└──
txt ─────┘└────┘ └──┘ └┘ └┘ ┴└──┘└┘ ┴└────┘ └┘└──┘└┘ ┴└──┘└┘└──
par ─────┘└────┘ └──┘ └┘ └┘ ┴└──┘└┘ ┴└────┘ └┘└──┘└┘ ┴└──┘└┘└──
pid ───────────┘ └──┘ └┘ └┘ └─────┘ └─────┘ └──────┘ └─────────
st ────────────────────────────┘└───┘└──┘└─────────────┘└──┘└───┘└┘┴└─
357 { simp at h,
src ─────┘└───────┘└─
typ ─────┘└───────┘└─
doc ─────┘└───────┘└─
txt ─────┘└───────┘└─
par ─────┘└───────┘└─
pid ─────────────────
st ──────────────┘└─
358 cases h,
id ┴
src ─────┘└────┘ └─
typ ─────┘└────┘┴└─
doc ─────┘└────┘ └─
txt ─────┘└────┘ └─
par ─────┘└────┘ └─
pid ───────────┘ └─
st ────────────┘└─
359 case or.inl : h { exact absurd h e },
id └────┘ ┴ ┴
src ───────────────────────┘└────┘└────┘┴ ┴ ┴└──
typ ───────────────────────┘└────┘└────┘┴┴┴┴┴└──
doc ───────────────────────┘└────┘ ┴ ┴ ┴└──
txt ───────────────────────┘└────┘ ┴ ┴ ┴└──
par ───────────────────────┘└────┘ ┴ ┴ ┴└──
pid ─────────────────────────────┘ ┴ ┴ └───
st ──────────────────────┘└────────────────┘┴└─
360 case or.inr : h {
src ────────────────────────
typ ────────────────────────
doc ────────────────────────
txt ────────────────────────
par ────────────────────────
pid ────────────────────────
st ────────────────────────
361 rcases ih h with ⟨b, tl₁, tl₂, h₁, h₂, h₃⟩,
id └┘ ┴
src ───────┘└─────┘ ┴ └─────────────────────────────┘└─
typ ───────┘└─────┘└┘┴┴└─────────────────────────────┘└─
doc ───────┘└─────┘ ┴ └─────────────────────────────┘└─
txt ───────┘└─────┘ ┴ └─────────────────────────────┘└─
par ───────┘└─────┘ ┴ └─────────────────────────────┘└─
pid ──────────────┘ ┴ └────────────────────────────────
st ─────────────────────────────────────────────────┘└─
362 exact ⟨b, hd :: tl₁, tl₂, not_mem_cons_of_ne_of_not_mem e h₁,
id ┴ └┘ └─┘ └─┘ └───────────────────────────┘ ┴ └┘
src ───────┘└────┘ └┘ ┴ ┴ └┘ └┘└───────────────────────────┘┴ ┴ └─
typ ───────┘└────┘ ┴└┘└┘┴ ┴└─┘└┘└─┘└┘└───────────────────────────┘┴┴┴└┘└─
doc ───────┘└────┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └─
txt ───────┘└────┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └─
par ───────┘└────┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └─
pid ─────────────┘ └┘ ┴ ┴ └┘ └┘ ┴ ┴ └─
st ──────────────────────────────────────────────────────────────────────
363 by rw h₂; refl, by simp [e, h₃]⟩ } } }
id └┘ ┴ └┘
src ──────────────┘ ┴└─┘ └┘└──┘└┘ ┴└────┘ └┘ ┴└┘└────┘
typ ──────────────┘ ┴└─┘└┘└┘└──┘└┘ ┴└────┘┴└┘└┘┴└┘└────┘
doc ──────────────┘ ┴└─┘ └┘└──┘└┘ ┴└────┘ └┘ ┴└┘└────┘
txt ──────────────┘ ┴└─┘ └┘└──┘└┘ ┴└────┘ └┘ ┴└┘└────┘
par ──────────────┘ ┴└─┘ └┘└──┘└┘ ┴└────┘ └┘ ┴└┘└────┘
pid ──────────────┘ └──┘ └──────┘ └─────┘ └┘ └──────┘┴
st ────────────────┘└──────────┘└──┘└───────────┘└┘┴┴└─┘┴
364 end
st └─┘
365
366 @[simp] theorem mem_keys_kerase_of_ne {a₁ a₂} {l : list (sigma β)} (h : a₁ ≠ a₂) :
id └──┘ └───┘ ┴ └┘ ┴ └┘
src └──┘ └───┘ ┴
typ └──┘ └───┘ ┴ └┘ ┴ └┘
doc └──┘
367 a₁ ∈ (kerase a₂ l).keys ↔ a₁ ∈ l.keys :=
id └┘ ┴ └────┘ └┘ ┴ └──┘ ┴ └┘ ┴ ┴└───┘
src ┴ └────┘ └──┘ ┴ ┴ └───┘
typ └┘ ┴ └────┘ └┘ ┴ └──┘ ┴ └┘ ┴ ┴└───┘
doc └────┘ └──┘ └───┘
368 iff.intro mem_keys_of_mem_keys_kerase $ λ p,
id └───────┘ └─────────────────────────┘ ┴
src └───────┘ └─────────────────────────┘
typ └───────┘ └─────────────────────────┘ ┴
369 if q : a₂ ∈ l.keys then
id └┘ └┘ ┴ ┴└───┘
src └┘ ┴ └───┘
typ └┘ └┘ ┴ ┴└───┘
doc └───┘
370 match l, kerase a₂ l, exists_of_kerase q, p with
id ┴ └────┘ └┘ ┴ └──────────────┘ ┴ ┴
src └────┘ └──────────────┘
typ ┴ └────┘ └┘ ┴ └──────────────┘ ┴ ┴
doc └────┘
371 | _, _, ⟨_, _, _, _, rfl, rfl⟩, p := by simpa [keys, h] using p
id └─┘ └──┘ ┴ ┴
src └─┘ └─────┘└──┘└┘ └──────┘ └
typ └─┘ └─────┘└──┘└┘┴└──────┘┴└
doc └─────┘└──┘└┘ └──────┘ └
txt └─────┘ └┘ └──────┘ └
par └─────┘ └┘ └──────┘ └
pid ┴┴ └┘ ┴┴└────┘ └
st └────────────────────────
372 end
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
373 else
374 by simp [q, p]
id ┴ ┴
src └────┘ └┘ └─
typ └────┘┴└┘┴└─
doc └────┘ └┘ └─
txt └────┘ └┘ └─
par └────┘ └┘ └─
pid ┴┴ └┘ ┴└
st └────────────
375
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
376 theorem keys_kerase {a} {l : list (sigma β)} : (kerase a l).keys = l.keys.erase a :=
id └──┘ └───┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴└───┘└────┘ ┴
src └──┘ └───┘ └────┘ └──┘ ┴ └───┘└────┘
typ └──┘ └───┘ ┴ └────┘ ┴ ┴ └──┘ ┴ ┴└───┘└────┘ ┴
doc └────┘ └──┘ └───┘
377 by rw [keys, kerase, ←erasep_map sigma.fst l, erase_eq_erasep]
id └──┘ └────┘ └────────┘ └───────┘ ┴ └─────────────┘
src └──┘└──┘└┘└────┘└─┘└────────┘┴└───────┘┴ └┘└─────────────┘└─
typ └──┘└──┘└┘└────┘└─┘└────────┘┴└───────┘┴┴└┘└─────────────┘└─
doc └──┘└──┘└┘└────┘└─┘ ┴ ┴ └┘ └─
txt └──┘ └┘ └─┘ ┴ ┴ └┘ └─
par └──┘ └┘ └─┘ ┴ ┴ └┘ └─
pid └┘ └┘ └─┘ ┴ ┴ └┘ ┴└
st └───────┘└──────┘└───────────────────────┘└───────────────┘┴└
378
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
379 theorem kerase_kerase {a a'} {l : list (sigma β)} : (kerase a' l).kerase a = (kerase a l).kerase a' :=
id └──┘ └───┘ ┴ └────┘ └┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ └┘
src └──┘ └───┘ └────┘ └────┘ ┴ └────┘ └────┘
typ └──┘ └───┘ ┴ └────┘ └┘ ┴ └────┘ ┴ ┴ └────┘ ┴ ┴ └────┘ └┘
doc └────┘ └────┘ └────┘ └────┘
380 begin
st └─────
381 by_cases a = a',
id ┴ ┴ └┘
src └───────┘ ┴┴┴
typ └───────┘┴┴┴┴└┘
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────┘└─
382 { subst a' },
id └┘
src └────┘ ┴
typ └────┘└┘┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└───────┘└┘└
383 induction l with x xs, { refl },
id ┴
src └────────┘ └────────┘ └───┘
typ └────────┘┴└────────┘ └───┘
doc └────────┘ └────────┘ └───┘
txt └────────┘ └────────┘ └───┘
par └────────┘ └────────┘ └───┘
pid ┴ ┴└───────┘ ┴
st ──────────────────────┘└──┘└───┘└┘└
384 { by_cases a' = x.1,
id └┘ ┴
src └───────┘ ┴ ┴ └┘
typ └───────┘└┘┴ ┴┴└┘
doc └───────┘ ┴ ┴ └┘
txt └───────┘ ┴ ┴ └┘
par └───────┘ ┴ ┴ └┘
pid ┴ ┴ ┴ └┘
st ────────────────────┘└─
385 { subst a', simp [kerase_cons_ne h,kerase_cons_eq rfl] },
id └┘ └────────────┘ ┴ └────────────┘ └─┘
src └────┘ └────┘└────────────┘┴ ┴└────────────┘┴└─┘└┘
typ └────┘└┘ └────┘└────────────┘┴┴┴└────────────┘┴└─┘└┘
doc └────┘ └────┘ ┴ ┴ ┴ └┘
txt └────┘ └────┘ ┴ ┴ ┴ └┘
par └────┘ └────┘ ┴ ┴ ┴ └┘
pid ┴ ┴┴ ┴ ┴ ┴ ┴┴
st ─────┘└──────┘└───────────────────────────────────────────┘└┘└
386 by_cases h' : a = x.1,
id ┴ ┴
src └───────┘ └─┘ ┴ ┴ └┘
typ └───────┘ └─┘┴┴ ┴┴└┘
doc └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ └┘
st ────────────────────────┘└─
387 { subst a, simp [kerase_cons_eq rfl,kerase_cons_ne (ne.symm h)] },
id ┴ └────────────┘ └─┘ └────────────┘ └─────┘ ┴
src └────┘ └────┘└────────────┘┴└─┘┴└────────────┘┴ └─────┘┴ └─┘
typ └────┘┴ └────┘└────────────┘┴└─┘┴└────────────┘┴ └─────┘┴┴└─┘
doc └────┘ └────┘ ┴ ┴ ┴ ┴ └─┘
txt └────┘ └────┘ ┴ ┴ ┴ ┴ └─┘
par └────┘ └────┘ ┴ ┴ ┴ ┴ └─┘
pid ┴ ┴┴ ┴ ┴ ┴ ┴ └┘┴
st ─────┘└─────┘└─────────────────────────────────────────────────────┘└┘└
388 { simp [kerase_cons_ne,*] } }
id └────────────┘
src └────┘└────────────┘└──┘
typ └────┘└────────────┘└──┘
doc └────┘ └──┘
txt └────┘ └──┘
par └────┘ └──┘
pid ┴┴ └─┘┴
st ─────────────────────────────┘└───
389 end
st ──┘
390
391 theorem kerase_nodupkeys (a : α) {l : list (sigma β)} : nodupkeys l → (kerase a l).nodupkeys :=
id ┴ └──┘ └───┘ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────┘
src └──┘ └───┘ └───────┘ └────┘ └───────┘
typ ┴ └──┘ └───┘ ┴ └───────┘ ┴ └────┘ ┴ ┴ └───────┘
doc └────┘
392 nodupkeys_of_sublist $ kerase_sublist _ _
id └──────────────────┘ └────────────┘
src └──────────────────┘ └────────────┘
typ └──────────────────┘ └────────────┘
393
394 theorem perm_kerase {a : α} {l₁ l₂ : list (sigma β)}
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
395 (nd : l₁.nodupkeys) : l₁ ~ l₂ → kerase a l₁ ~ kerase a l₂ :=
id └┘└────────┘ └┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
src └────────┘ ┴ └────┘ ┴ └────┘
typ └┘└────────┘ └┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
doc ┴ └────┘ ┴ └────┘
396 perm_erasep _ $ (nodupkeys_iff_pairwise.1 nd).imp $
id └─────────┘ └────────────────────┘┴ └┘ └─┘
src └─────────┘ └────────────────────┘┴ └─┘
typ └─────────┘ └────────────────────┘┴ └┘ └─┘
397 by rintro x y h rfl; exact h
id ┴
src └──────────────┘ └────┘ └
typ └──────────────┘ └────┘┴└
doc └──────────────┘ └────┘ └
txt └──────────────┘ └────┘ └
par └──────────────┘ └────┘ └
pid └────────┘ ┴ └
st └──────────────────────────
398
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
399 @[simp] theorem not_mem_keys_kerase (a) {l : list (sigma β)} (nd : l.nodupkeys) :
id └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ └──┘ └───┘ ┴ ┴└────────┘
doc └──┘
400 a ∉ (kerase a l).keys :=
id ┴ ┴ └────┘ ┴ ┴ └──┘
src ┴ └────┘ └──┘
typ ┴ ┴ └────┘ ┴ ┴ └──┘
doc └────┘ └──┘
401 begin
st └─────
402 induction l,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────┘└─
403 case list.nil { simp },
src └──────────────┘└───┘┴
typ └──────────────┘└───┘┴
doc └──────────────┘└───┘┴
txt └──────────────┘└───┘┴
par └──────────────┘└───┘┴
pid └───────┘┴└──────┘
st ────────────────┘└────┘└┘└
404 case list.cons : hd tl ih {
src └───────────────────────────
typ └───────────────────────────
doc └───────────────────────────
txt └───────────────────────────
par └───────────────────────────
pid └────────┘└─────────┘└──
st ────────────────────────────┘└
405 simp at nd,
src ───┘└────────┘└─
typ ───┘└────────┘└─
doc ───┘└────────┘└─
txt ───┘└────────┘└─
par ───┘└────────┘└─
pid ────────────────
st ─────────────┘└─
406 by_cases h : a = hd.1,
id ┴ ┴ └┘
src ───┘└───────┘ └─┘ ┴┴┴ └┘└─
typ ───┘└───────┘ └─┘┴┴┴┴└┘└┘└─
doc ───┘└───────┘ └─┘ ┴ ┴ └┘└─
txt ───┘└───────┘ └─┘ ┴ ┴ └┘└─
par ───┘└───────┘ └─┘ ┴ ┴ └┘└─
pid ────────────┘ └─┘ ┴ ┴ └───
st ────────────────────────┘└─
407 { subst h, simp [nd.1] },
id ┴ └┘
src ─────┘└────┘ └┘└────┘ └──┘└──
typ ─────┘└────┘┴└┘└────┘└┘└──┘└──
doc ─────┘└────┘ └┘└────┘ └──┘└──
txt ─────┘└────┘ └┘└────┘ └──┘└──
par ─────┘└────┘ └┘└────┘ └──┘└──
pid ───────────┘ └──────┘ └──────
st ────┘└──────┘└────────────┘┴└─
408 { simp [h, ih nd.2] } }
id ┴ └┘ └┘
src ─────┘└────┘ └┘ ┴ └──┘└──┘
typ ─────┘└────┘┴└┘└┘┴└┘└──┘└──┘
doc ─────┘└────┘ └┘ ┴ └──┘└──┘
txt ─────┘└────┘ └┘ ┴ └──┘└──┘
par ─────┘└────┘ └┘ ┴ └──┘└──┘
pid ───────────┘ └┘ ┴ └─────┘┴
st ───────────────────────┘└─┘┴
409 end
st └─┘
410
411 @[simp] theorem lookup_kerase (a) {l : list (sigma β)} (nd : l.nodupkeys) :
id └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ └──┘ └───┘ ┴ ┴└────────┘
doc └──┘
412 lookup a (kerase a l) = none :=
id └────┘ ┴ └────┘ ┴ ┴ ┴ └──┘
src └────┘ └────┘ ┴ └──┘
typ └────┘ ┴ └────┘ ┴ ┴ ┴ └──┘
doc └────┘ └────┘
413 lookup_eq_none.mpr (not_mem_keys_kerase a nd)
id └────────────┘└──┘ └─────────────────┘ ┴ └┘
src └────────────┘└──┘ └─────────────────┘
typ └────────────┘└──┘ └─────────────────┘ ┴ └┘
414
415 @[simp] theorem lookup_kerase_ne {a a'} {l : list (sigma β)} (h : a ≠ a') :
id └──┘ └───┘ ┴ ┴ ┴ └┘
src └──┘ └───┘ ┴
typ └──┘ └───┘ ┴ ┴ ┴ └┘
doc └──┘
416 lookup a (kerase a' l) = lookup a l :=
id └────┘ ┴ └────┘ └┘ ┴ ┴ └────┘ ┴ ┴
src └────┘ └────┘ ┴ └────┘
typ └────┘ ┴ └────┘ └┘ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └────┘ └────┘
417 begin
st └─────
418 induction l,
id ┴
src └────────┘
typ └────────┘┴
doc └────────┘
txt └────────┘
par └────────┘
pid ┴
st ────────────┘└─
419 case list.nil { refl },
src └──────────────┘└───┘┴
typ └──────────────┘└───┘┴
doc └──────────────┘└───┘┴
txt └──────────────┘└───┘┴
par └──────────────┘└───┘┴
pid └───────┘┴└──────┘
st ────────────────┘└────┘└┘└
420 case list.cons : hd tl ih {
src └───────────────────────────
typ └───────────────────────────
doc └───────────────────────────
txt └───────────────────────────
par └───────────────────────────
pid └────────┘└─────────┘└──
st ────────────────────────────┘└
421 cases hd with ah bh,
id └┘
src ───┘└────┘ └─────────┘└─
typ ───┘└────┘└┘└─────────┘└─
doc ───┘└────┘ └─────────┘└─
txt ───┘└────┘ └─────────┘└─
par ───┘└────┘ └─────────┘└─
pid ─────────┘ └────────────
st ──────────────────────┘└─
422 by_cases h₁ : a = ah; by_cases h₂ : a' = ah,
id ┴ ┴ └┘ └┘ └┘
src ───┘└───────┘ └─┘ ┴┴┴ └┘└───────┘ └─┘ ┴ ┴ └─
typ ───┘└───────┘ └─┘┴┴┴┴└┘└┘└───────┘ └─┘└┘┴ ┴└┘└─
doc ───┘└───────┘ └─┘ ┴ ┴ └┘└───────┘ └─┘ ┴ ┴ └─
txt ───┘└───────┘ └─┘ ┴ ┴ └┘└───────┘ └─┘ ┴ ┴ └─
par ───┘└───────┘ └─┘ ┴ ┴ └┘└───────┘ └─┘ ┴ ┴ └─
pid ────────────┘ └─┘ ┴ ┴ └─────────┘ └─┘ ┴ ┴ └─
st ──────────────────────────────────────────────┘└─
423 { substs h₁ h₂, cases ne.irrefl h },
id └───────┘ ┴
src ─────┘└──────────┘└┘└────┘└───────┘┴ ┴└──
typ ─────┘└──────────┘└┘└────┘└───────┘┴┴┴└──
doc ─────┘└──────────┘└┘└────┘ ┴ ┴└──
txt ─────┘└──────────┘└┘└────┘ ┴ ┴└──
par ─────┘└──────────┘└┘└────┘ ┴ ┴└──
pid ─────────────────────────┘ ┴ └───
st ────┘└───────────┘└──────────────────┘┴└─
424 { subst h₁, simp [h₂] },
id └┘ └┘
src ─────┘└────┘ └┘└────┘ └┘└──
typ ─────┘└────┘└┘└┘└────┘└┘└┘└──
doc ─────┘└────┘ └┘└────┘ └┘└──
txt ─────┘└────┘ └┘└────┘ └┘└──
par ─────┘└────┘ └┘└────┘ └┘└──
pid ───────────┘ └──────┘ └────
st ────┘└───────┘└──────────┘┴└─
425 { subst h₂, simp [h] },
id └┘ ┴
src ─────┘└────┘ └┘└────┘ └┘└──
typ ─────┘└────┘└┘└┘└────┘┴└┘└──
doc ─────┘└────┘ └┘└────┘ └┘└──
txt ─────┘└────┘ └┘└────┘ └┘└──
par ─────┘└────┘ └┘└────┘ └┘└──
pid ───────────┘ └──────┘ └────
st ────┘└───────┘└─────────┘┴└─
426 { simp [h₁, h₂, ih] }
id └┘ └┘ └┘
src ─────┘└────┘ └┘ └┘ └┘└─
typ ─────┘└────┘└┘└┘└┘└┘└┘└┘└─
doc ─────┘└────┘ └┘ └┘ └┘└─
txt ─────┘└────┘ └┘ └┘ └┘└─
par ─────┘└────┘ └┘ └┘ └┘└─
pid ───────────┘ └┘ └┘ └───
st ───────────────────────┘└─
427 }
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ──┘┴
st ──┘┴
428 end
st └─┘
429
430 theorem kerase_append_left {a} : ∀ {l₁ l₂ : list (sigma β)},
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
431 a ∈ l₁.keys → kerase a (l₁ ++ l₂) = kerase a l₁ ++ l₂
id ┴ ┴ └┘└───┘ └────┘ ┴ └┘ └┘ └┘ ┴ └────┘ ┴ └┘ └┘ └┘
src ┴ └───┘ └────┘ └┘ ┴ └────┘ └┘
typ ┴ ┴ └┘└───┘ └────┘ ┴ └┘ └┘ └┘ ┴ └────┘ ┴ └┘ └┘ └┘
doc └───┘ └────┘ └────┘
432 | [] _ h := by cases h
id └┘ ┴
src └┘ └────┘ ┴
typ └┘ └────┘┴┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st └───────┘
433 | (s :: l₁) l₂ h₁ :=
id ┴ └┘
src └┘
typ ┴ └┘
434 if h₂ : a = s.1 then
id └┘ ┴ ┴ ┴
src └┘ ┴ ┴
typ └┘ ┴ ┴ ┴
435 by simp [h₂]
id └┘
src └────┘ └─
typ └────┘└┘└─
doc └────┘ └─
txt └────┘ └─
par └────┘ └─
pid ┴┴ ┴└
st └──────────
436 else
src ─┘
typ ─┘
doc ─┘
txt ─┘
par ─┘
pid ─┘
st ─┘
437 by simp at h₁;
src └────────┘
typ └────────┘
doc └────────┘
txt └────────┘
par └────────┘
pid ┴└───┘
st └────────────
438 cases h₁;
id └┘
src └────┘
typ └────┘└┘
doc └────┘
txt └────┘
par └────┘
pid ┴
st ─────────────────
439 [exact absurd h₁ h₂, simp [h₂, kerase_append_left h₁]]
id ┴ └────┘ └┘ └┘ └┘ └────────────────┘ └┘
src ┴└────┘└────┘┴ ┴ └────┘ └┘ ┴ ┴
typ ┴└────┘└────┘┴└┘┴└┘ └────┘└┘└┘└────────────────┘┴└┘┴
doc └────┘ ┴ ┴ └────┘ └┘ ┴ ┴
txt └────┘ ┴ ┴ └────┘ └┘ ┴ ┴
par └────┘ ┴ ┴ └────┘ └┘ ┴ ┴
pid ┴ ┴ ┴ ┴┴ └┘ ┴ ┴
st ────────────────────────────────────────────────────────────┘
440
441 theorem kerase_append_right {a} : ∀ {l₁ l₂ : list (sigma β)},
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
442 a ∉ l₁.keys → kerase a (l₁ ++ l₂) = l₁ ++ kerase a l₂
id ┴ ┴ └┘└───┘ └────┘ ┴ └┘ └┘ └┘ ┴ └┘ └┘ └────┘ ┴ └┘
src ┴ └───┘ └────┘ └┘ ┴ └┘ └────┘
typ ┴ ┴ └┘└───┘ └────┘ ┴ └┘ └┘ └┘ ┴ └┘ └┘ └────┘ ┴ └┘
doc └───┘ └────┘ └────┘
443 | [] _ h := rfl
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
444 | (_ :: l₁) l₂ h := by simp [not_or_distrib] at h;
id └┘ └────────────┘
src └┘ └────┘└────────────┘└────┘
typ └┘ └────┘└────────────┘└────┘
doc └────┘ └────┘
txt └────┘ └────┘
par └────┘ └────┘
pid ┴┴ ┴┴└──┘
st └────────────────────────────
445 simp [h.1, kerase_append_right h.2]
id ┴ └─────────────────┘ ┴
src └────┘ └──┘ ┴ └───
typ └────┘┴└──┘└─────────────────┘┴┴└───
doc └────┘ └──┘ ┴ └───
txt └────┘ └──┘ ┴ └───
par └────┘ └──┘ ┴ └───
pid ┴┴ └──┘ ┴ └─┘└
st ───────────────────────────────────────────────────────────
446
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
447 theorem kerase_comm (a₁ a₂) (l : list (sigma β)) :
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
448 kerase a₂ (kerase a₁ l) = kerase a₁ (kerase a₂ l) :=
id └────┘ └┘ └────┘ └┘ ┴ ┴ └────┘ └┘ └────┘ └┘ ┴
src └────┘ └────┘ ┴ └────┘ └────┘
typ └────┘ └┘ └────┘ └┘ ┴ ┴ └────┘ └┘ └────┘ └┘ ┴
doc └────┘ └────┘ └────┘ └────┘
449 if h : a₁ = a₂ then
id └┘ └┘ ┴ └┘
src └┘ ┴
typ └┘ └┘ ┴ └┘
450 by simp [h]
id ┴
src └────┘ └┘
typ └────┘┴└┘
doc └────┘ └┘
txt └────┘ └┘
par └────┘ └┘
pid ┴┴ ┴┴
st └────────┘
451 else if ha₁ : a₁ ∈ l.keys then
id └┘ └┘ ┴ ┴└───┘
src └┘ ┴ └───┘
typ └┘ └┘ ┴ ┴└───┘
doc └───┘
452 if ha₂ : a₂ ∈ l.keys then
id └┘ └┘ ┴ ┴└───┘
src └┘ ┴ └───┘
typ └┘ └┘ ┴ ┴└───┘
doc └───┘
453 match l, kerase a₁ l, exists_of_kerase ha₁, ha₂ with
id ┴ └────┘ └┘ ┴ └──────────────┘ └─┘ └─┘
src └────┘ └──────────────┘
typ ┴ └────┘ └┘ ┴ └──────────────┘ └─┘ └─┘
doc └────┘
454 | _, _, ⟨b₁, l₁, l₂, a₁_nin_l₁, rfl, rfl⟩, a₂_in_l₁_app_l₂ :=
id └┘ └─┘
src └─┘
typ └┘ └─┘
455 if h' : a₂ ∈ l₁.keys then
id └┘ └┘ ┴ └───┘
src └┘ ┴ └───┘
typ └┘ └┘ ┴ └───┘
doc └───┘
456 by simp [kerase_append_left h',
id └────────────────┘ └┘
src └────┘└────────────────┘┴ └─
typ └────┘└────────────────┘┴└┘└─
doc └────┘ ┴ └─
txt └────┘ ┴ └─
par └────┘ ┴ └─
pid ┴┴ ┴ └─
st └─────────────────────────────
457 kerase_append_right (mt (mem_keys_kerase_of_ne h).mp a₁_nin_l₁)]
id └─────────────────┘ └┘ └───────────────────┘ ┴ └───────┘
src ────────────────┘└─────────────────┘┴ └┘┴ └───────────────────┘┴ └───┘ └──
typ ────────────────┘└─────────────────┘┴ └┘┴ └───────────────────┘┴┴└───┘└───────┘└──
doc ────────────────┘ ┴ ┴ ┴ └───┘ └──
txt ────────────────┘ ┴ ┴ ┴ └───┘ └──
par ────────────────┘ ┴ ┴ ┴ └───┘ └──
pid ────────────────┘ ┴ ┴ ┴ └───┘ └┘└
st ──────────────────────────────────────────────────────────────────────────────────
458 else
src ─────┘
typ ─────┘
doc ─────┘
txt ─────┘
par ─────┘
pid ─────┘
st ─────┘
459 by simp [kerase_append_right h', kerase_append_right a₁_nin_l₁,
id └─────────────────┘ └┘ └─────────────────┘ └───────┘
src └────┘└─────────────────┘┴ └┘└─────────────────┘┴ └─
typ └────┘└─────────────────┘┴└┘└┘└─────────────────┘┴└───────┘└─
doc └────┘ ┴ └┘ ┴ └─
txt └────┘ ┴ └┘ ┴ └─
par └────┘ ┴ └┘ ┴ └─
pid ┴┴ ┴ └┘ ┴ └─
st └─────────────────────────────────────────────────────────────
460 @kerase_cons_ne _ _ _ a₂ ⟨a₁, b₁⟩ _ (ne.symm h)]
id └────────────┘ └┘ └┘ └┘ └─────┘ ┴
src ────────────────┘ └────────────┘└─────┘ ┴ └┘ └──┘ └─────┘┴ └──
typ ────────────────┘ └────────────┘└─────┘└┘┴ └┘└┘└┘└──┘ └─────┘┴┴└──
doc ────────────────┘ └─────┘ ┴ └┘ └──┘ ┴ └──
txt ────────────────┘ └─────┘ ┴ └┘ └──┘ ┴ └──
par ────────────────┘ └─────┘ ┴ └┘ └──┘ ┴ └──
pid ────────────────┘ └─────┘ ┴ └┘ └──┘ ┴ └┘└
st ──────────────────────────────────────────────────────────────────
461 end
src ───┘
typ ───┘
doc ───┘
txt ───┘
par ───┘
pid ───┘
st ───┘
462 else
463 by simp [ha₂, mt mem_keys_of_mem_keys_kerase ha₂]
id └─┘ └┘ └─────────────────────────┘ └─┘
src └────┘ └┘└┘┴└─────────────────────────┘┴ └┘
typ └────┘└─┘└┘└┘┴└─────────────────────────┘┴└─┘└┘
doc └────┘ └┘ ┴ ┴ └┘
txt └────┘ └┘ ┴ ┴ └┘
par └────┘ └┘ ┴ ┴ └┘
pid ┴┴ └┘ ┴ ┴ ┴┴
st └──────────────────────────────────────────────┘
464 else
465 by simp [ha₁, mt mem_keys_of_mem_keys_kerase ha₁]
id └─┘ └┘ └─────────────────────────┘ └─┘
src └────┘ └┘└┘┴└─────────────────────────┘┴ └─
typ └────┘└─┘└┘└┘┴└─────────────────────────┘┴└─┘└─
doc └────┘ └┘ ┴ ┴ └─
txt └────┘ └┘ ┴ ┴ └─
par └────┘ └┘ ┴ ┴ └─
pid ┴┴ └┘ ┴ ┴ ┴└
st └───────────────────────────────────────────────
466
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
467 /- kinsert -/
src ──────────────
typ ──────────────
doc ──────────────
txt ──────────────
par ──────────────
pid ──────────────
st ──────────────
468
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
469 /-- Insert the pair `⟨a, b⟩` and erase the first pair with the key `a`. -/
470 def kinsert (a : α) (b : β a) (l : list (sigma β)) : list (sigma β) :=
id ┴ ┴ ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
src └──┘ └───┘ └──┘ └───┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
471 ⟨a, b⟩ :: kerase a l
id ┴ ┴ └┘ └────┘ ┴ ┴
src └┘ └────┘
typ ┴ ┴ └┘ └────┘ ┴ ┴
doc └────┘
472
473 @[simp] theorem kinsert_def {a} {b : β a} {l : list (sigma β)} :
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
doc └──┘
474 kinsert a b l = ⟨a, b⟩ :: kerase a l := rfl
id └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────┘ ┴ ┴ └─┘
src └─────┘ ┴ └┘ └────┘ └─┘
typ └─────┘ ┴ ┴ ┴ ┴ ┴ ┴ └┘ └────┘ ┴ ┴ └─┘
doc └─────┘ └────┘
475
476 @[simp] theorem mem_keys_kinsert {a a'} {b' : β a'} {l : list (sigma β)} :
id ┴ └┘ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └┘ └──┘ └───┘ ┴
doc └──┘
477 a ∈ (kinsert a' b' l).keys ↔ a = a' ∨ a ∈ l.keys :=
id ┴ ┴ └─────┘ └┘ └┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└───┘
src ┴ └─────┘ └──┘ ┴ ┴ ┴ ┴ └───┘
typ ┴ ┴ └─────┘ └┘ └┘ ┴ └──┘ ┴ ┴ ┴ └┘ ┴ ┴ ┴ ┴└───┘
doc └─────┘ └──┘ └───┘
478 by by_cases h : a = a'; simp [h]
id ┴ ┴ └┘ ┴
src └───────┘ └─┘ ┴┴┴ └────┘ └─
typ └───────┘ └─┘┴┴┴┴└┘ └────┘┴└─
doc └───────┘ └─┘ ┴ ┴ └────┘ └─
txt └───────┘ └─┘ ┴ ┴ └────┘ └─
par └───────┘ └─┘ ┴ ┴ └────┘ └─
pid ┴ └─┘ ┴ ┴ ┴┴ ┴└
st └──────────────────────────────
479
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
480 theorem kinsert_nodupkeys (a) (b : β a) {l : list (sigma β)} (nd : l.nodupkeys) :
id ┴ ┴ └──┘ └───┘ ┴ ┴└────────┘
src └──┘ └───┘ └────────┘
typ ┴ ┴ └──┘ └───┘ ┴ ┴└────────┘
481 (kinsert a b l).nodupkeys :=
id └─────┘ ┴ ┴ ┴ └───────┘
src └─────┘ └───────┘
typ └─────┘ ┴ ┴ ┴ └───────┘
doc └─────┘
482 nodupkeys_cons.mpr ⟨not_mem_keys_kerase a nd, kerase_nodupkeys a nd⟩
id └────────────┘└──┘ └─────────────────┘ ┴ └┘ └──────────────┘ ┴ └┘
src └────────────┘└──┘ └─────────────────┘ └──────────────┘
typ └────────────┘└──┘ └─────────────────┘ ┴ └┘ └──────────────┘ ┴ └┘
483
484 theorem perm_kinsert {a} {b : β a} {l₁ l₂ : list (sigma β)} (nd₁ : l₁.nodupkeys)
id ┴ ┴ └──┘ └───┘ ┴ └┘└────────┘
src └──┘ └───┘ └────────┘
typ ┴ ┴ └──┘ └───┘ ┴ └┘└────────┘
485 (p : l₁ ~ l₂) : kinsert a b l₁ ~ kinsert a b l₂ :=
id └┘ ┴ └┘ └─────┘ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ └┘
src ┴ └─────┘ ┴ └─────┘
typ └┘ ┴ └┘ └─────┘ ┴ ┴ └┘ ┴ └─────┘ ┴ ┴ └┘
doc ┴ └─────┘ ┴ └─────┘
486 perm.skip ⟨a, b⟩ $ perm_kerase nd₁ p
id └───────┘ ┴ ┴ └─────────┘ └─┘ ┴
src └───────┘ └─────────┘
typ └───────┘ ┴ ┴ └─────────┘ └─┘ ┴
487
488 @[simp] theorem lookup_kinsert {a} {b : β a} (l : list (sigma β)) :
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
doc └──┘
489 lookup a (kinsert a b l) = some b :=
id └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴
src └────┘ └─────┘ ┴ └──┘
typ └────┘ ┴ └─────┘ ┴ ┴ ┴ ┴ └──┘ ┴
doc └────┘ └─────┘
490 by simp only [kinsert, lookup_cons_eq]
id └─────┘ └────────────┘
src └─────────┘└─────┘└┘└────────────┘└─
typ └─────────┘└─────┘└┘└────────────┘└─
doc └─────────┘└─────┘└┘ └─
txt └─────────┘ └┘ └─
par └─────────┘ └┘ └─
pid ┴└──┘└┘ └┘ ┴└
st └────────────────────────────────────
491
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
492 @[simp] theorem lookup_kinsert_ne {a a'} {b' : β a'} {l : list (sigma β)} (h : a ≠ a') :
id ┴ └┘ └──┘ └───┘ ┴ ┴ ┴ └┘
src └──┘ └───┘ ┴
typ ┴ └┘ └──┘ └───┘ ┴ ┴ ┴ └┘
doc └──┘
493 lookup a (kinsert a' b' l) = lookup a l :=
id └────┘ ┴ └─────┘ └┘ └┘ ┴ ┴ └────┘ ┴ ┴
src └────┘ └─────┘ ┴ └────┘
typ └────┘ ┴ └─────┘ └┘ └┘ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └─────┘ └────┘
494 by simp [h, lookup_cons_ne _ ⟨a', b'⟩ h]
id ┴ └────────────┘ └┘ └┘ ┴
src └────┘ └┘└────────────┘└─┘ └┘ └┘ └─
typ └────┘┴└┘└────────────┘└─┘ └┘└┘└┘└┘┴└─
doc └────┘ └┘ └─┘ └┘ └┘ └─
txt └────┘ └┘ └─┘ └┘ └┘ └─
par └────┘ └┘ └─┘ └┘ └┘ └─
pid ┴┴ └┘ └─┘ └┘ └┘ ┴└
st └──────────────────────────────────────
495
src ─
typ ─
doc ─
txt ─
par ─
pid ─
st ─
496 /- kextract -/
src ───────────────
typ ───────────────
doc ───────────────
txt ───────────────
par ───────────────
pid ───────────────
st ───────────────
497
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
498 def kextract (a : α) : list (sigma β) → option (β a) × list (sigma β)
id ┴ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘ └────┘ ┴ └──┘ └───┘
typ ┴ └──┘ └───┘ ┴ ┴ └────┘ ┴ ┴ ┴ └──┘ └───┘ ┴
499 | [] := (none, [])
id └┘ ┴└──┘ └┘
src └┘ ┴└──┘ └┘
typ └┘ ┴└──┘ └┘
500 | (s::l) := if h : s.1 = a then (some (eq.rec_on h s.2), l) else
id ┴└┘┴ └┘ ┴ ┴ ┴ ┴└──┘ └───────┘ ┴ ┴
src └┘ └┘ ┴ ┴ ┴└──┘ └───────┘ ┴
typ ┴└┘┴ └┘ ┴ ┴ ┴ ┴└──┘ └───────┘ ┴ ┴
501 let (b', l') := kextract l in (b', s :: l')
id └─┘ ┴└┘ └┘ └──────┘ ┴ └┘
src ┴ ┴ └┘
typ └─┘ ┴└┘ └┘ └──────┘ ┴ └┘
502
503 @[simp] theorem kextract_eq_lookup_kerase (a : α) :
id ┴
typ ┴
doc └──┘
504 ∀ l : list (sigma β), kextract a l = (lookup a l, kerase a l)
id ┴ └──┘ └───┘ ┴ └──────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ └────┘ ┴ ┴
src └──┘ └───┘ └──────┘ ┴ ┴└────┘ └────┘
typ ┴ └──┘ └───┘ ┴ └──────┘ ┴ ┴ ┴ ┴└────┘ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
505 | [] := rfl
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
506 | (⟨a', b⟩::l) := begin
id └┘
src └┘
typ └┘
st └─────
507 simp [kextract], dsimp, split_ifs,
id └──────┘
src └────┘└──────┘┴ └───┘ └───────┘
typ └────┘└──────┘┴ └───┘ └───────┘
doc └────┘ ┴ └───┘ └───────┘
txt └────┘ ┴ └───┘ └───────┘
par └────┘ ┴ └───┘ └───────┘
pid ┴┴ ┴
st ──────────────────┘└─────┘└─────────┘└─
508 { subst a', simp [kerase] },
id └┘ └────┘
src └────┘ └────┘└────┘└┘
typ └────┘└┘ └────┘└────┘└┘
doc └────┘ └────┘└────┘└┘
txt └────┘ └────┘ └┘
par └────┘ └────┘ └┘
pid ┴ ┴┴ ┴┴
st ─────┘└──────┘└──────────────┘└┘└
509 { simp [kextract, ne.symm h, kextract_eq_lookup_kerase l, kerase] }
id └──────┘ └─────┘ ┴ └───────────────────────┘ ┴ └────┘
src └────┘└──────┘└┘└─────┘┴ └┘ ┴ └┘└────┘└┘
typ └────┘└──────┘└┘└─────┘┴┴└┘└───────────────────────┘┴┴└┘└────┘└┘
doc └────┘ └┘ ┴ └┘ ┴ └┘└────┘└┘
txt └────┘ └┘ ┴ └┘ ┴ └┘ └┘
par └────┘ └┘ ┴ └┘ ┴ └┘ └┘
pid ┴┴ └┘ ┴ └┘ ┴ └┘ ┴┴
st ─────────────────────────────────────────────────────────────────────┘└─
510 end
st ────┘
511
512 /- erase_dupkeys -/
513
514 def erase_dupkeys : list (sigma β) → list (sigma β) :=
id └──┘ └───┘ ┴ └──┘ └───┘ ┴
src └──┘ └───┘ └──┘ └───┘
typ └──┘ └───┘ ┴ └──┘ └───┘ ┴
515 list.foldr (λ ⟨x,y⟩, kinsert x y) []
id └────────┘ ┴┴ ┴ └─────┘ └┘
src └────────┘ └─────┘ └┘
typ └────────┘ ┴┴ ┴ └─────┘ └┘
doc └─────┘
516
517 lemma erase_dupkeys_cons {x : α} {y : β x} (l : list (sigma β)) : erase_dupkeys (⟨x,y⟩ :: l) = kinsert x y (erase_dupkeys l) := rfl
id ┴ ┴ ┴ └──┘ └───┘ ┴ └───────────┘ ┴ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴ └───────────┘ ┴ └─┘
src └──┘ └───┘ └───────────┘ └┘ ┴ └─────┘ └───────────┘ └─┘
typ ┴ ┴ ┴ └──┘ └───┘ ┴ └───────────┘ ┴ ┴ └┘ ┴ ┴ └─────┘ ┴ ┴ └───────────┘ ┴ └─┘
doc └─────┘
518
519 lemma nodupkeys_erase_dupkeys (l : list (sigma β)) : nodupkeys (erase_dupkeys l) :=
id └──┘ └───┘ ┴ └───────┘ └───────────┘ ┴
src └──┘ └───┘ └───────┘ └───────────┘
typ └──┘ └───┘ ┴ └───────┘ └───────────┘ ┴
520 begin
st └─────
521 dsimp [erase_dupkeys], generalize hl : nil = l',
id └───────────┘ └─┘
src └─────┘└───────────┘┴ └──────────────┘└─┘┴ ┴
typ └─────┘└───────────┘┴ └──────────────┘└─┘┴ ┴
doc └─────┘ ┴ └──────────────┘ ┴ ┴
txt └─────┘ ┴ └──────────────┘ ┴ ┴
par └─────┘ ┴ └──────────────┘ ┴ ┴
pid ┴┴ ┴ └─┘└┘┴ ┴ ┴
st ──────────────────────┘└────────────────────────┘└─
522 have : nodupkeys l', { rw ← hl, apply nodup_nil },
id └───────┘ └┘ └┘ └───────┘
src └─────┘└───────┘┴ └───┘ └────┘└───────┘┴
typ └─────┘└───────┘┴└┘ └───┘└┘ └────┘└───────┘┴
doc └─────┘ ┴ └───┘ └────┘ ┴
txt └─────┘ ┴ └───┘ └────┘ ┴
par └─────┘ ┴ └───┘ └────┘ ┴
pid └───┘└┘ ┴ └─┘ ┴ ┴
st ────────────────────┘└──┘└─────┘└────────────────┘└┘└
523 clear hl,
src └──────┘
typ └──────┘
doc └──────┘
txt └──────┘
par └──────┘
pid └─┘
st ─────────┘└─
524 induction l with x xs,
id ┴
src └────────┘ └────────┘
typ └────────┘┴└────────┘
doc └────────┘ └────────┘
txt └────────┘ └────────┘
par └────────┘ └────────┘
pid ┴ ┴└───────┘
st ──────────────────────┘└─
525 { apply this },
src └────┘ ┴
typ └────┘ ┴
doc └────┘ ┴
txt └────┘ ┴
par └────┘ ┴
pid ┴ ┴
st ───┘└─────────┘└┘└
526 { cases x, simp [erase_dupkeys], split,
id ┴ └───────────┘
src └────┘ └────┘└───────────┘┴ └───┘
typ └────┘┴ └────┘└───────────┘┴ └───┘
doc └────┘ └────┘ ┴ └───┘
txt └────┘ └────┘ ┴ └───┘
par └────┘ └────┘ ┴ └───┘
pid ┴ ┴┴ ┴
st ──────────┘└────────────────────┘└─────┘└─
527 { simp [keys_kerase], apply mem_erase_of_nodup l_ih },
id └─────────┘ └────────────────┘ └──┘
src └────┘└─────────┘┴ └────┘└────────────────┘┴ ┴
typ └────┘└─────────┘┴ └────┘└────────────────┘┴└──┘┴
doc └────┘ ┴ └────┘ ┴ ┴
txt └────┘ ┴ └────┘ ┴ ┴
par └────┘ ┴ └────┘ ┴ ┴
pid ┴┴ ┴ ┴ ┴ ┴
st ─────┘└────────────────┘└──────────────────────────────┘└┘└
528 apply kerase_nodupkeys _ l_ih, }
id └──────────────┘ └──┘
src └────┘└──────────────┘└─┘
typ └────┘└──────────────┘└─┘└──┘
doc └────┘ └─┘
txt └────┘ └─┘
par └────┘ └─┘
pid ┴ └─┘
st ────────────────────────────────┘└───
529 end
st ──┘
530
531 lemma lookup_erase_dupkeys (a : α) (l : list (sigma β)) : lookup a (erase_dupkeys l) = lookup a l :=
id ┴ └──┘ └───┘ ┴ └────┘ ┴ └───────────┘ ┴ ┴ └────┘ ┴ ┴
src └──┘ └───┘ └────┘ └───────────┘ ┴ └────┘
typ ┴ └──┘ └───┘ ┴ └────┘ ┴ └───────────┘ ┴ ┴ └────┘ ┴ ┴
doc └────┘ └────┘
532 begin
st └─────
533 induction l, refl,
id ┴
src └────────┘ └──┘
typ └────────┘┴ └──┘
doc └────────┘ └──┘
txt └────────┘ └──┘
par └────────┘ └──┘
pid ┴
st ────────────┘└────┘└─
534 cases l_hd with a' b,
id └──┘
src └────┘ └────────┘
typ └────┘└──┘└────────┘
doc └────┘ └────────┘
txt └────┘ └────────┘
par └────┘ └────────┘
pid ┴ └────────┘
st ─────────────────────┘└─
535 by_cases a = a',
id ┴ ┴ └┘
src └───────┘ ┴┴┴
typ └───────┘┴┴┴┴└┘
doc └───────┘ ┴ ┴
txt └───────┘ ┴ ┴
par └───────┘ ┴ ┴
pid ┴ ┴ ┴
st ────────────────┘└─
536 { subst a', rw [erase_dupkeys_cons,lookup_kinsert,lookup_cons_eq] },
id └┘ └────────────────┘ └────────────┘ └────────────┘
src └────┘ └──┘└────────────────┘┴└────────────┘┴└────────────┘└┘
typ └────┘└┘ └──┘└────────────────┘┴└────────────┘┴└────────────┘└┘
doc └────┘ └──┘ ┴ ┴ └┘
txt └────┘ └──┘ ┴ ┴ └┘
par └────┘ └──┘ ┴ ┴ └┘
pid ┴ └┘ ┴ ┴ ┴┴
st ───┘└──────┘└──────────────────────┘└─────────────┘└─────────────┘┴┴└┘└
537 { rw [erase_dupkeys_cons,lookup_kinsert_ne h,l_ih,lookup_cons_ne], exact h },
id └────────────────┘ └───────────────┘ ┴ └──┘ └────────────┘ ┴
src └──┘└────────────────┘┴└───────────────┘┴ ┴ ┴└────────────┘┴ └────┘ ┴
typ └──┘└────────────────┘┴└───────────────┘┴┴┴└──┘┴└────────────┘┴ └────┘┴┴
doc └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
txt └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
par └──┘ ┴ ┴ ┴ ┴ ┴ └────┘ ┴
pid └┘ ┴ ┴ ┴ ┴ ┴ ┴ ┴
st ─────────────────────────┘└──────────────────┘└───┘└─────────────┘└─────────┘└──
538 end
st ──┘
539
540 /- kunion -/
541
542 /-- `kunion l₁ l₂` is the append to l₁ of l₂ after, for each key in l₁, the
543 first matching pair in l₂ is erased. -/
544 def kunion : list (sigma β) → list (sigma β) → list (sigma β)
id └──┘ └───┘ ┴ ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
src └──┘ └───┘ └──┘ └───┘ └──┘ └───┘
typ └──┘ └───┘ ┴ ┴ └──┘ └───┘ ┴ └──┘ └───┘ ┴
545 | [] l₂ := l₂
id └┘ └┘
src └┘
typ └┘ └┘
546 | (s :: l₁) l₂ := s :: kunion l₁ (kerase s.1 l₂)
id ┴ └┘ └┘ └┘ └┘ └────┘ └────┘ ┴
src └┘ └┘ └────┘ ┴
typ ┴ └┘ └┘ └┘ └┘ └────┘ └────┘ ┴
doc └────┘
547
548 @[simp] theorem nil_kunion {l : list (sigma β)} : kunion [] l = l :=
id └──┘ └───┘ ┴ └────┘ └┘ ┴ ┴ ┴
src └──┘ └───┘ └────┘ └┘ ┴
typ └──┘ └───┘ ┴ └────┘ └┘ ┴ ┴ ┴
doc └──┘ └────┘
549 rfl
id └─┘
src └─┘
typ └─┘
550
551 @[simp] theorem kunion_nil : ∀ {l : list (sigma β)}, kunion l [] = l
id ┴ └──┘ └───┘ ┴ └────┘ ┴ └┘ ┴ ┴
src └──┘ └───┘ └────┘ └┘ ┴
typ ┴ └──┘ └───┘ ┴ └────┘ ┴ └┘ ┴ ┴
doc └──┘ └────┘
552 | [] := rfl
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
553 | (_ :: l) := by rw [kunion, kerase_nil, kunion_nil]
id └┘ └────┘ └────────┘
src └┘ └──┘└────┘└┘└────────┘└┘ └─
typ └┘ └──┘└────┘└┘└────────┘└┘└────────┘└─
doc └──┘└────┘└┘ └┘ └─
txt └──┘ └┘ └┘ └─
par └──┘ └┘ └┘ └─
pid └┘ └┘ └┘ ┴└
st └─────────┘└──────────┘└──────────┘┴└
554
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
555 @[simp] theorem kunion_cons {s} {l₁ l₂ : list (sigma β)} :
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
doc └──┘
556 kunion (s :: l₁) l₂ = s :: kunion l₁ (kerase s.1 l₂) :=
id └────┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └────┘ └┘ └────┘ ┴┴ └┘
src └────┘ └┘ ┴ └┘ └────┘ └────┘ ┴
typ └────┘ ┴ └┘ └┘ └┘ ┴ ┴ └┘ └────┘ └┘ └────┘ ┴┴ └┘
doc └────┘ └────┘ └────┘
557 rfl
id └─┘
src └─┘
typ └─┘
558
559 @[simp] theorem mem_keys_kunion {a} {l₁ l₂ : list (sigma β)} :
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
doc └──┘
560 a ∈ (kunion l₁ l₂).keys ↔ a ∈ l₁.keys ∨ a ∈ l₂.keys :=
id ┴ ┴ └────┘ └┘ └┘ └──┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ └┘└───┘
src ┴ └────┘ └──┘ ┴ ┴ └───┘ ┴ ┴ └───┘
typ ┴ ┴ └────┘ └┘ └┘ └──┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ └┘└───┘
doc └────┘ └──┘ └───┘ └───┘
561 begin
st └─────
562 induction l₁ generalizing l₂,
id └┘
src └────────┘ └──────────────┘
typ └────────┘└┘└──────────────┘
doc └────────┘ └──────────────┘
txt └────────┘ └──────────────┘
par └────────┘ └──────────────┘
pid ┴ ┴└─────────────┘
st ─────────────────────────────┘└─
563 case list.nil { simp },
src └──────────────┘└───┘┴
typ └──────────────┘└───┘┴
doc └──────────────┘└───┘┴
txt └──────────────┘└───┘┴
par └──────────────┘└───┘┴
pid └───────┘┴└──────┘
st ────────────────┘└────┘└┘└
564 case list.cons : s l₁ ih { by_cases h : a = s.1; [simp [h], simp [h, ih]] }
id ┴ ┴ ┴ ┴ ┴
src └─────────────────────────┘└───────┘ └─┘ ┴┴┴ └┘└─┘└────┘ ┴└┘└────┘ └┘ ┴└──┘
typ └─────────────────────────┘└───────┘ └─┘┴┴┴┴┴└┘└─┘└────┘┴┴└┘└────┘┴└┘└┘┴└──┘
doc └─────────────────────────┘└───────┘ └─┘ ┴ ┴ └┘└─┘└────┘ ┴└┘└────┘ └┘ ┴└──┘
txt └─────────────────────────┘└───────┘ └─┘ ┴ ┴ └┘└─┘└────┘ ┴└┘└────┘ └┘ ┴└──┘
par └─────────────────────────┘└───────┘ └─┘ ┴ ┴ └┘└─┘└────┘ ┴└┘└────┘ └┘ ┴└──┘
pid └────────┘└────────┘└──────────┘ └─┘ ┴ ┴ └─────────┘ └───────┘ └┘ └──┘┴
st ───────────────────────────┘└─────────────────────────────────────────────┘└┘┴
565 end
st └─┘
566
567 @[simp] theorem kunion_kerase {a} : ∀ {l₁ l₂ : list (sigma β)},
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
doc └──┘
568 kunion (kerase a l₁) (kerase a l₂) = kerase a (kunion l₁ l₂)
id └────┘ └────┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └────┘ └┘ └┘
src └────┘ └────┘ └────┘ ┴ └────┘ └────┘
typ └────┘ └────┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └────┘ └┘ └┘
doc └────┘ └────┘ └────┘ └────┘ └────┘
569 | [] _ := rfl
id └┘ └─┘
src └┘ └─┘
typ └┘ └─┘
570 | (s :: _) l := by by_cases h : a = s.1;
id └┘ ┴ ┴ ┴
src └┘ └───────┘ └─┘ ┴┴┴ └┘
typ └┘ └───────┘ └─┘┴┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴ └┘
txt └───────┘ └─┘ ┴ ┴ └┘
par └───────┘ └─┘ ┴ ┴ └┘
pid ┴ └─┘ ┴ ┴ └┘
st └──────────────────────
571 simp [h, kerase_comm a s.1 l, kunion_kerase]
id ┴ └─────────┘ ┴ ┴ ┴
src └────┘ └┘└─────────┘┴ ┴ └─┘ └┘ └─
typ └────┘┴└┘└─────────┘┴┴┴┴└─┘┴└┘└───────────┘└─
doc └────┘ └┘ ┴ ┴ └─┘ └┘ └─
txt └────┘ └┘ ┴ ┴ └─┘ └┘ └─
par └────┘ └┘ ┴ ┴ └─┘ └┘ └─
pid ┴┴ └┘ ┴ ┴ └─┘ └┘ ┴└
st ────────────────────────────────────────────────────────────────
572
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
573 theorem kunion_nodupkeys {l₁ l₂ : list (sigma β)}
id └──┘ └───┘ ┴
src └──┘ └───┘
typ └──┘ └───┘ ┴
574 (nd₁ : l₁.nodupkeys) (nd₂ : l₂.nodupkeys) : (kunion l₁ l₂).nodupkeys :=
id └┘└────────┘ └┘└────────┘ └────┘ └┘ └┘ └───────┘
src └────────┘ └────────┘ └────┘ └───────┘
typ └┘└────────┘ └┘└────────┘ └────┘ └┘ └┘ └───────┘
doc └────┘
575 begin
st └─────
576 induction l₁ generalizing l₂,
id └┘
src └────────┘ └──────────────┘
typ └────────┘└┘└──────────────┘
doc └────────┘ └──────────────┘
txt └────────┘ └──────────────┘
par └────────┘ └──────────────┘
pid ┴ ┴└─────────────┘
st ─────────────────────────────┘└─
577 case list.nil { simp only [nil_kunion, nd₂] },
id └────────┘ └─┘
src └──────────────┘└─────────┘└────────┘└┘ └┘┴
typ └──────────────┘└─────────┘└────────┘└┘└─┘└┘┴
doc └──────────────┘└─────────┘ └┘ └┘┴
txt └──────────────┘└─────────┘ └┘ └┘┴
par └──────────────┘└─────────┘ └┘ └┘┴
pid └───────┘┴└───────────┘ └┘ └─┘
st ────────────────┘└───────────────────────────┘└┘└
578 case list.cons : s l₁ ih {
src └──────────────────────────
typ └──────────────────────────
doc └──────────────────────────
txt └──────────────────────────
par └──────────────────────────
pid └────────┘└────────┘└──
st ───────────────────────────┘└
579 simp at nd₁,
src ───┘└─────────┘└─
typ ───┘└─────────┘└─
doc ───┘└─────────┘└─
txt ───┘└─────────┘└─
par ───┘└─────────┘└─
pid ─────────────────
st ──────────────┘└─
580 simp [not_or_distrib, nd₁.1, nd₂, ih nd₁.2 (kerase_nodupkeys s.1 nd₂)] }
id └────────────┘ └─┘ └─┘ └┘ └─┘ └──────────────┘ ┴ └─┘
src ───┘└────┘└────────────┘└┘ └──┘ └┘ ┴ └─┘ └──────────────┘┴ └─┘ └─┘└┘
typ ───┘└────┘└────────────┘└┘└─┘└──┘└─┘└┘└┘┴└─┘└─┘ └──────────────┘┴┴└─┘└─┘└─┘└┘
doc ───┘└────┘ └┘ └──┘ └┘ ┴ └─┘ ┴ └─┘ └─┘└┘
txt ───┘└────┘ └┘ └──┘ └┘ ┴ └─┘ ┴ └─┘ └─┘└┘
par ───┘└────┘ └┘ └──┘ └┘ ┴ └─┘ ┴ └─┘ └─┘└┘
pid ─────────┘ └┘ └──┘ └┘ ┴ └─┘ ┴ └─┘ └──┘┴
st ──────────────────────────────────────────────────────────────────────────┘┴┴
581 end
st └─┘
582
583 theorem perm_kunion_left {l₁ l₂ : list (sigma β)} (p : l₁ ~ l₂) (l) :
id └──┘ └───┘ ┴ └┘ ┴ └┘
src └──┘ └───┘ ┴
typ └──┘ └───┘ ┴ └┘ ┴ └┘
doc ┴
584 kunion l₁ l ~ kunion l₂ l :=
id └────┘ └┘ ┴ ┴ └────┘ └┘ ┴
src └────┘ ┴ └────┘
typ └────┘ └┘ ┴ ┴ └────┘ └┘ ┴
doc └────┘ ┴ └────┘
585 begin
st └─────
586 induction p generalizing l,
id ┴
src └────────┘ └─────────────┘
typ └────────┘┴└─────────────┘
doc └────────┘ └─────────────┘
txt └────────┘ └─────────────┘
par └────────┘ └─────────────┘
pid ┴ ┴└────────────┘
st ───────────────────────────┘└─
587 case list.perm.nil { refl },
src └───────────────────┘└───┘┴
typ └───────────────────┘└───┘┴
doc └───────────────────┘└───┘┴
txt └───────────────────┘└───┘┴
par └───────────────────┘└───┘┴
pid └────────────┘┴└──────┘
st ─────────────────────┘└────┘└┘└
588 case list.perm.skip : hd tl₁ tl₂ p ih {
src └───────────────────────────────────────
typ └───────────────────────────────────────
doc └───────────────────────────────────────
txt └───────────────────────────────────────
par └───────────────────────────────────────
pid └─────────────┘└────────────────┘└──
st ────────────────────────────────────────┘└
589 simp [ih (kerase hd.1 l), perm.skip] },
id └┘ └────┘ └┘ ┴ └───────┘
src ───┘└────┘ ┴ └────┘┴ └─┘ └─┘└───────┘└┘┴
typ ───┘└────┘└┘┴ └────┘┴└┘└─┘┴└─┘└───────┘└┘┴
doc ───┘└────┘ ┴ └────┘┴ └─┘ └─┘ └┘┴
txt ───┘└────┘ ┴ ┴ └─┘ └─┘ └┘┴
par ───┘└────┘ ┴ ┴ └─┘ └─┘ └┘┴
pid ─────────┘ ┴ ┴ └─┘ └─┘ └─┘
st ────────────────────────────────────────┘└┘└
590 case list.perm.swap : s₁ s₂ l {
src └───────────────────────────────
typ └───────────────────────────────
doc └───────────────────────────────
txt └───────────────────────────────
par └───────────────────────────────
pid └─────────────┘└────────┘└──
st ────────────────────────────────┘└
591 simp [kerase_comm, perm.swap] },
id └─────────┘ └───────┘
src ───┘└────┘└─────────┘└┘└───────┘└┘┴
typ ───┘└────┘└─────────┘└┘└───────┘└┘┴
doc ───┘└────┘ └┘ └┘┴
txt ───┘└────┘ └┘ └┘┴
par ───┘└────┘ └┘ └┘┴
pid ─────────┘ └┘ └─┘
st ─────────────────────────────────┘└┘└
592 case list.perm.trans : l₁ l₂ l₃ p₁₂ p₂₃ ih₁₂ ih₂₃ {
src └───────────────────────────────────────────────────
typ └───────────────────────────────────────────────────
doc └───────────────────────────────────────────────────
txt └───────────────────────────────────────────────────
par └───────────────────────────────────────────────────
pid └──────────────┘└───────────────────────────┘└──
st ────────────────────────────────────────────────────┘└
593 exact perm.trans (ih₁₂ l) (ih₂₃ l) }
id └────────┘ └──┘ └──┘ ┴
src ───┘└────┘└────────┘┴ ┴ └┘ ┴ └┘└┘
typ ───┘└────┘└────────┘┴ └──┘┴ └┘ └──┘┴┴└┘└┘
doc ───┘└────┘ ┴ ┴ └┘ ┴ └┘└┘
txt ───┘└────┘ ┴ ┴ └┘ ┴ └┘└┘
par ───┘└────┘ ┴ ┴ └┘ ┴ └┘└┘
pid ─────────┘ ┴ ┴ └┘ ┴ └─┘┴
st ──────────────────────────────────────┘┴┴
594 end
st └─┘
595
596 theorem perm_kunion_right : ∀ l {l₁ l₂ : list (sigma β)},
id ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ └──┘ └───┘ ┴
597 l₁.nodupkeys → l₁ ~ l₂ → kunion l l₁ ~ kunion l l₂
id └┘└────────┘ └┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
src └────────┘ ┴ └────┘ ┴ └────┘
typ └┘└────────┘ └┘ ┴ └┘ └────┘ ┴ └┘ ┴ └────┘ ┴ └┘
doc ┴ └────┘ ┴ └────┘
598 | [] _ _ _ p := p
id └┘ ┴
src └┘
typ └┘ ┴
599 | (s :: l) l₁ l₂ nd₁ p :=
id └┘
src └┘
typ └┘
600 by simp [perm.skip s
id └───────┘
src └────┘└───────┘┴ └
typ └────┘└───────┘┴ └
doc └────┘ ┴ └
txt └────┘ ┴ └
par └────┘ ┴ └
pid ┴┴ ┴ └
st └──────────────────
601 (perm_kunion_right l (kerase_nodupkeys s.1 nd₁) (perm_kerase nd₁ p))]
id └───────────────┘ ┴ └──────────────┘ ┴ └─────────┘ └─┘ ┴
src ───┘ ┴ ┴ └──────────────┘┴ └─┘ └┘ └─────────┘┴ ┴ └───
typ ───┘ └───────────────┘┴┴┴ └──────────────┘┴┴└─┘ └┘ └─────────┘┴└─┘┴┴└───
doc ───┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └───
txt ───┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └───
par ───┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └───
pid ───┘ ┴ ┴ ┴ └─┘ └┘ ┴ ┴ └─┘└
st ──────────────────────────────────────────────────────────────────────────
602
src ┘
typ ┘
doc ┘
txt ┘
par ┘
pid ┘
st ┘
603 theorem perm_kunion {l₁ l₂ l₃ l₄ : list (sigma β)} (nd₃ : l₃.nodupkeys)
id └──┘ └───┘ ┴ └┘└────────┘
src └──┘ └───┘ └────────┘
typ └──┘ └───┘ ┴ └┘└────────┘
604 (p₁₂ : l₁ ~ l₂) (p₃₄ : l₃ ~ l₄) : kunion l₁ l₃ ~ kunion l₂ l₄ :=
id └┘ ┴ └┘ └┘ ┴ └┘ └────┘ └┘ └┘ ┴ └────┘ └┘ └┘
src ┴ ┴ └────┘ ┴ └────┘
typ └┘ ┴ └┘ └┘ ┴ └┘ └────┘ └┘ └┘ ┴ └────┘ └┘ └┘
doc ┴ ┴ └────┘ ┴ └────┘
605 perm.trans (perm_kunion_left p₁₂ l₃) (perm_kunion_right l₂ nd₃ p₃₄)
id └────────┘ └──────────────┘ └─┘ └┘ └───────────────┘ └┘ └─┘ └─┘
src └────────┘ └──────────────┘ └───────────────┘
typ └────────┘ └──────────────┘ └─┘ └┘ └───────────────┘ └┘ └─┘ └─┘
606
607 @[simp] theorem lookup_kunion_left {a} {l₁ l₂ : list (sigma β)} (h : a ∈ l₁.keys) :
id └──┘ └───┘ ┴ ┴ ┴ └┘└───┘
src └──┘ └───┘ ┴ └───┘
typ └──┘ └───┘ ┴ ┴ ┴ └┘└───┘
doc └──┘ └───┘
608 lookup a (kunion l₁ l₂) = lookup a l₁ :=
id └────┘ ┴ └────┘ └┘ └┘ ┴ └────┘ ┴ └┘
src └────┘ └────┘ ┴ └────┘
typ └────┘ ┴ └────┘ └┘ └┘ ┴ └────┘ ┴ └┘
doc └────┘ └────┘ └────┘
609 begin
st └─────
610 induction l₁ with s _ ih generalizing l₂; simp at h; cases h; cases s with a',
id └┘ ┴ ┴
src └────────┘ └──────────────────────────┘ └───────┘ └────┘ └────┘ └──────┘
typ └────────┘└┘└──────────────────────────┘ └───────┘ └────┘┴ └────┘┴└──────┘
doc └────────┘ └──────────────────────────┘ └───────┘ └────┘ └────┘ └──────┘
txt └────────┘ └──────────────────────────┘ └───────┘ └────┘ └────┘ └──────┘
par └────────┘ └──────────────────────────┘ └───────┘ └────┘ └────┘ └──────┘
pid ┴ ┴└─────────┘└──────────────┘ ┴└──┘ ┴ ┴ └──────┘
st ──────────────────────────────────────────────────────────────────────────────┘└─
611 { subst h, simp },
id ┴
src └────┘ └───┘
typ └────┘┴ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ───┘└─────┘└─────┘└┘└
612 { rw kunion_cons,
id └─────────┘
src └─┘└─────────┘
typ └─┘└─────────┘
doc └─┘
txt └─┘
par └─┘
pid ┴
st ─────────────────┘└─
613 by_cases h' : a = a',
id ┴ ┴ └┘
src └───────┘ └─┘ ┴┴┴
typ └───────┘ └─┘┴┴┴┴└┘
doc └───────┘ └─┘ ┴ ┴
txt └───────┘ └─┘ ┴ ┴
par └───────┘ └─┘ ┴ ┴
pid ┴ └─┘ ┴ ┴
st ───────────────────────┘└─
614 { subst h', simp },
id └┘
src └────┘ └───┘
typ └────┘└┘ └───┘
doc └────┘ └───┘
txt └────┘ └───┘
par └────┘ └───┘
pid ┴ ┴
st ─────┘└──────┘└─────┘└┘└
615 { simp [h', ih h] } }
id └┘ └┘ ┴
src └────┘ └┘ ┴ └┘
typ └────┘└┘└┘└┘┴┴└┘
doc └────┘ └┘ ┴ └┘
txt └────┘ └┘ ┴ └┘
par └────┘ └┘ ┴ └┘
pid ┴┴ └┘ ┴ ┴┴
st ─────────────────────┘└───
616 end
st ──┘
617
618 @[simp] theorem lookup_kunion_right {a} {l₁ l₂ : list (sigma β)} (h : a ∉ l₁.keys) :
id └──┘ └───┘ ┴ ┴ ┴ └┘└───┘
src └──┘ └───┘ ┴ └───┘
typ └──┘ └───┘ ┴ ┴ ┴ └┘└───┘
doc └──┘ └───┘
619 lookup a (kunion l₁ l₂) = lookup a l₂ :=
id └────┘ ┴ └────┘ └┘ └┘ ┴ └────┘ ┴ └┘
src └────┘ └────┘ ┴ └────┘
typ └────┘ ┴ └────┘ └┘ └┘ ┴ └────┘ ┴ └┘
doc └────┘ └────┘ └────┘
620 begin
st └─────
621 induction l₁ generalizing l₂,
id └┘
src └────────┘ └──────────────┘
typ └────────┘└┘└──────────────┘
doc └────────┘ └──────────────┘
txt └────────┘ └──────────────┘
par └────────┘ └──────────────┘
pid ┴ ┴└─────────────┘
st ─────────────────────────────┘└─
622 case list.nil { simp },
src └──────────────┘└───┘┴
typ └──────────────┘└───┘┴
doc └──────────────┘└───┘┴
txt └──────────────┘└───┘┴
par └──────────────┘└───┘┴
pid └───────┘┴└──────┘
st ────────────────┘└────┘└┘└
623 case list.cons : _ _ ih { simp [not_or_distrib] at h, simp [h.1, ih h.2] }
id └────────────┘ ┴ └┘ ┴
src └────────────────────────┘└────┘└────────────┘└────┘└┘└────┘ └──┘ ┴ └──┘└┘
typ └────────────────────────┘└────┘└────────────┘└────┘└┘└────┘┴└──┘└┘┴┴└──┘└┘
doc └────────────────────────┘└────┘ └────┘└┘└────┘ └──┘ ┴ └──┘└┘
txt └────────────────────────┘└────┘ └────┘└┘└────┘ └──┘ ┴ └──┘└┘
par └────────────────────────┘└────┘ └────┘└┘└────┘ └──┘ ┴ └──┘└┘
pid └────────┘└───────┘└───────┘ └────────────┘ └──┘ ┴ └───┘┴
st ──────────────────────────┘└─────────────────────────┘└───────────────────┘┴┴
624 end
st └─┘
625
626 @[simp] theorem mem_lookup_kunion {a} {b : β a} {l₁ l₂ : list (sigma β)} :
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
doc └──┘
627 b ∈ lookup a (kunion l₁ l₂) ↔ b ∈ lookup a l₁ ∨ a ∉ l₁.keys ∧ b ∈ lookup a l₂ :=
id ┴ ┴ └────┘ ┴ └────┘ └┘ └┘ ┴ ┴ ┴ └────┘ ┴ └┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ └────┘ ┴ └┘
src ┴ └────┘ └────┘ ┴ ┴ └────┘ ┴ ┴ └───┘ ┴ ┴ └────┘
typ ┴ ┴ └────┘ ┴ └────┘ └┘ └┘ ┴ ┴ ┴ └────┘ ┴ └┘ ┴ ┴ ┴ └┘└───┘ ┴ ┴ ┴ └────┘ ┴ └┘
doc └────┘ └────┘ └────┘ └───┘ └────┘
628 begin
st └─────
629 induction l₁ generalizing l₂,
id └┘
src └────────┘ └──────────────┘
typ └────────┘└┘└──────────────┘
doc └────────┘ └──────────────┘
txt └────────┘ └──────────────┘
par └────────┘ └──────────────┘
pid ┴ ┴└─────────────┘
st ─────────────────────────────┘└─
630 case list.nil { simp },
src └──────────────┘└───┘┴
typ └──────────────┘└───┘┴
doc └──────────────┘└───┘┴
txt └──────────────┘└───┘┴
par └──────────────┘└───┘┴
pid └───────┘┴└──────┘
st ────────────────┘└────┘└┘└
631 case list.cons : s _ ih {
src └─────────────────────────
typ └─────────────────────────
doc └─────────────────────────
txt └─────────────────────────
par └─────────────────────────
pid └────────┘└───────┘└──
st ──────────────────────────┘└
632 cases s with a',
id ┴
src ───┘└────┘ └──────┘└─
typ ───┘└────┘┴└──────┘└─
doc ───┘└────┘ └──────┘└─
txt ───┘└────┘ └──────┘└─
par ───┘└────┘ └──────┘└─
pid ─────────┘ └─────────
st ──────────────────┘└─
633 by_cases h₁ : a = a',
id ┴ ┴ └┘
src ───┘└───────┘ └─┘ ┴┴┴ └─
typ ───┘└───────┘ └─┘┴┴┴┴└┘└─
doc ───┘└───────┘ └─┘ ┴ ┴ └─
txt ───┘└───────┘ └─┘ ┴ ┴ └─
par ───┘└───────┘ └─┘ ┴ ┴ └─
pid ────────────┘ └─┘ ┴ ┴ └─
st ───────────────────────┘└─
634 { subst h₁, simp },
id └┘
src ─────┘└────┘ └┘└───┘└──
typ ─────┘└────┘└┘└┘└───┘└──
doc ─────┘└────┘ └┘└───┘└──
txt ─────┘└────┘ └┘└───┘└──
par ─────┘└────┘ └┘└───┘└──
pid ───────────┘ └─────────
st ────┘└───────┘└─────┘┴└─
635 { let h₂ := @ih (kerase a' l₂), simp [h₁] at h₂, simp [h₁, h₂] } }
id └┘ └────┘ └┘ └┘ └┘ └┘ └┘
src ─────┘└────────┘ ┴ └────┘┴ ┴ ┴└┘└────┘ └─────┘└┘└────┘ └┘ └┘└──┘
typ ─────┘└────────┘ └┘┴ └────┘┴└┘┴└┘┴└┘└────┘└┘└─────┘└┘└────┘└┘└┘└┘└┘└──┘
doc ─────┘└────────┘ ┴ └────┘┴ ┴ ┴└┘└────┘ └─────┘└┘└────┘ └┘ └┘└──┘
txt ─────┘└────────┘ ┴ ┴ ┴ ┴└┘└────┘ └─────┘└┘└────┘ └┘ └┘└──┘
par ─────┘└────────┘ ┴ ┴ ┴ ┴└┘└────┘ └─────┘└┘└────┘ └┘ └┘└──┘
pid ───────────────┘ ┴ ┴ ┴ └───────┘ └─────────────┘ └┘ └───┘┴
st ─────────────────────────────────┘└───────────────┘└──────────────┘└─┘┴
636 end
st └─┘
637
638 theorem mem_lookup_kunion_middle {a} {b : β a} {l₁ l₂ l₃ : list (sigma β)}
id ┴ ┴ └──┘ └───┘ ┴
src └──┘ └───┘
typ ┴ ┴ └──┘ └───┘ ┴
639 (h₁ : b ∈ lookup a (kunion l₁ l₃)) (h₂ : a ∉ keys l₂) :
id ┴ ┴ └────┘ ┴ └────┘ └┘ └┘ ┴ ┴ └──┘ └┘
src ┴ └────┘ └────┘ ┴ └──┘
typ ┴ ┴ └────┘ ┴ └────┘ └┘ └┘ ┴ ┴ └──┘ └┘
doc └────┘ └────┘ └──┘
640 b ∈ lookup a (kunion (kunion l₁ l₂) l₃) :=
id ┴ ┴ └────┘ ┴ └────┘ └────┘ └┘ └┘ └┘
src ┴ └────┘ └────┘ └────┘
typ ┴ ┴ └────┘ ┴ └────┘ └────┘ └┘ └┘ └┘
doc └────┘ └────┘ └────┘
641 match mem_lookup_kunion.mp h₁ with
id └───────────────┘└─┘ └┘
src └───────────────┘└─┘
typ └───────────────┘└─┘ └┘
642 | or.inl h := mem_lookup_kunion.mpr (or.inl (mem_lookup_kunion.mpr (or.inl h)))
id └────┘ ┴ └───────────────┘└──┘ └────┘ └───────────────┘└──┘ └────┘
src └────┘ └───────────────┘└──┘ └────┘ └───────────────┘└──┘ └────┘
typ └────┘ ┴ └───────────────┘└──┘ └────┘ └───────────────┘└──┘ └────┘
643 | or.inr h := mem_lookup_kunion.mpr $
id └────┘ ┴ └───────────────┘└──┘
src └────┘ └───────────────┘└──┘
typ └────┘ ┴ └───────────────┘└──┘
644 or.inr ⟨mt mem_keys_kunion.mp (not_or_distrib.mpr ⟨h.1, h₂⟩), h.2⟩
id └────┘ └┘ └─────────────┘└─┘ └────────────┘└──┘ ┴ └┘ ┴
src └────┘ └┘ └─────────────┘└─┘ └────────────┘└──┘ ┴ ┴
typ └────┘ └┘ └─────────────┘└─┘ └────────────┘└──┘ ┴ └┘ ┴
645 end
646
647 end list